P. 7 of Theorem List - bfol.mm Proof Explorer

Theorem List for bfol.mm Proof Explorer - 601-700   *Has distinct variable group(s)

Type	Label	Description
Statement
6.1.4  More Quantifier Laws.
Theorem	alloverimex-P5 601	Alternate version of alloverim-P5 588 that produces existential quantifiers.
⊢ (𝛾 → ∀𝑥(𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	alloverimex-P5.RC 602	Inference Form of alloverimex-P5 601.
⊢ ∀𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	alloverimex-P5.RC.GEN 603	Inference Form of alloverimex-P5 601 with Generalization. For the deductive form with a variable restriction, see alloverimex-P5.GENV 622. For the most general form see alloverimex-P5.GENF 748.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	alloverimex-P5.CL 604	Closed Form of alloverimex-P5 601.
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	dalloverimex-P5 605	Alternate version of dalloverim-P5 590 that produces existential quantifiers.
⊢ (𝛾 → ∀𝑥(𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	dalloverimex-P5.RC 606	Inference Form of dalloverimex-P5 605.
⊢ ∀𝑥(𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	dalloverimex-P5.RC.GEN 607	Inference Form of dalloverimex-P5 605 with Generalization.
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
6.1.4.1  A Substitution Law for Existential Quantification.
Theorem	subexinf-P5 608	Inference Version of '∃𝑥' Substitution Law. For the deductive form with a variable restriction see subexv-P5 624. For the most general form see subex-P6 754.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
6.1.5  Quantified Implication Equivalence Laws.
Theorem	qimeqallhalf-P5 609	Partial Quantified Implication Equivalence Law ( ( E → U ) → U ). The reverse implication is only true when '𝑥' either does not occur in '𝜑' (qimeqallav-P5 618) or '𝜓' (qimeqallbv-P5 620), or does not occur free in '𝜑' (qimeqalla-P6 699) or '𝜓' (qimeqallb-P6 701).
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	qimeqex-P5-L1 610	Lemma for qimeqex-P5 612. [Auxiliary lemma - not displayed.]
Theorem	qimeqex-P5-L2 611	Lemma for qimeqex-P5 612. [Auxiliary lemma - not displayed.]
Theorem	qimeqex-P5 612	Quantified Implication Equivalence Law ( E ↔ ( U → E ) ).
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
6.2  Consequences of ax-L5.
Theorem	axL5ex-P5 613*	Dual of ax-L5 17. '𝑥' does not occur in '𝜑'.
⊢ (∃𝑥𝜑 → 𝜑)
Theorem	allicv-P5 614*	Introduction of Universal Quantifier as Consequent. (variable restriction). '𝑥' may occur in '𝜓' but not '𝜑'. This is a weak version of the '∀' intruduction rule in the natural deduction system. The version with a non-freeness condition is allic-P6 745.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	exiav-P5 615*	Introduction of Existential Quantifier as Antecedent (variable restriction). '𝑥' may occur in '𝜑', but not '𝜓'. This is a weaker version of the '∃' elimination rule in the natural deduction system. The version with a non-freeness condition is exia-P6 746.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exiav-P5.SH 616*	Inference Form of exiav-P5 615.
⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	qimeqallav-P5-L1 617*	Lemma for qimeqallav-P5 618. [Auxiliary lemma - not displayed.]
Theorem	qimeqallav-P5 618*	First Bi-directional Form of qimeqallhalf-P5 609 ( U ↔ ( E → U ) ) (variable restriction a). Holds when '𝑥' does not occur in '𝜑'. The most general version is qimeqalla-P6 699.
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qimeqallbv-P5-L1 619*	Lemma for qimeqallbv-P5 620. [Auxiliary lemma - not displayed.]
Theorem	qimeqallbv-P5 620*	Second Bi-directional Form of qimeqallhalf-P5 609 ( U ↔ ( E → U ) ) (variable restriction b). Holds when '𝑥' does not occur in '𝜓'. The most general version is qimeqallb-P6 701.
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
6.2.1  Generalization Augmentation with Context.
Theorem	alloverim-P5.GENV 621*	alloverim-P5 588 with Generalization (variable restriction). The most general form is alloverim-P5.GENF 747.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverimex-P5.GENV 622*	alloverimex-P5 601 with Generalization (variable restriction). The most general form is alloverimex-P5.GENF 748.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
6.2.2  Substitution Laws for Quantifiers.
Theorem	suballv-P5 623*	Substitution Law for '∀𝑥' (variable restriction). The most general form is suball-P6 753.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	subexv-P5 624*	Substitution Law for '∃𝑥' (variable restriction). The most general form is subex-P6 754.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
6.3  Consequences of Axioms Involving Equality ( ax-L6 - ax-L9 ).
Theorem	axL6ex-P5 625*	Existential Form of ax-L6 18.
⊢ ∃𝑥 𝑥 = 𝑡
6.3.1  Equivalence Properties of Equality Predicate. Show that '=' is an equivalence relation.
Theorem	eqref-P5 626	Equivalence Property: '=' Reflexivity.
⊢ 𝑡 = 𝑡
Theorem	eqsym-P5 627	Equivalence Property: '=' symmetry.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → 𝑢 = 𝑡)
Theorem	eqsym-P5.CL 628	Closed Form of eqsym-P5 627.
⊢ (𝑡 = 𝑢 → 𝑢 = 𝑡)
Theorem	eqsym-P5.CL.SYM 629	Closed Symmetric Form of eqsym-P5 627.
⊢ (𝑡 = 𝑢 ↔ 𝑢 = 𝑡)
Theorem	eqtrns-P5 630	Equivalence Property: '=' Transitivity.
⊢ (𝛾 → 𝑡 = 𝑢)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → 𝑡 = 𝑤)
Theorem	eqtrns-P5.CL 631	Closed Form of eqtrns-P5 630.
⊢ ((𝑡 = 𝑢 ∧ 𝑢 = 𝑤) → 𝑡 = 𝑤)
6.3.2  More Substitution Laws.
6.3.2.1  Substitution Laws for Equality.
Theorem	subeql-P5 632	Left Substitution Law for '=' .
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 = 𝑤 ↔ 𝑢 = 𝑤))
Theorem	subeql-P5.CL 633	Closed Form of subeql-P5 632.
⊢ (𝑡 = 𝑢 → (𝑡 = 𝑤 ↔ 𝑢 = 𝑤))
Theorem	subeqr-P5-L1 634	Lemma for subeqr-P5 635. [Auxiliary lemma - not displayed.]
Theorem	subeqr-P5 635	Right Substitution Law for '=' .
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 = 𝑡 ↔ 𝑤 = 𝑢))
Theorem	subeqr-P5.CL 636	Closed Form of subeqr-P5 635.
⊢ (𝑡 = 𝑢 → (𝑤 = 𝑡 ↔ 𝑤 = 𝑢))
Theorem	subeqd-P5 637	Dual Substitution Law for '='.
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 = 𝑢 ↔ 𝑡 = 𝑤))
6.3.2.2  Substitution Laws for Primitive Predicate.
Theorem	subelofl-P5 638	Left Substitution for '∈'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 ∈ 𝑤 ↔ 𝑢 ∈ 𝑤))
Theorem	subelofl-P5.CL 639	Closed Form of subelofl-P5.CL 639
⊢ (𝑡 = 𝑢 → (𝑡 ∈ 𝑤 ↔ 𝑢 ∈ 𝑤))
Theorem	subelofr-P5 640	Right Substitution for '∈'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑢))
Theorem	subelofr-P5.CL 641	Closed Form of subelofr-P5.CL 641
⊢ (𝑡 = 𝑢 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑢))
Theorem	subelofd-P5 642	Dual Substitution for '∈'.
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 ∈ 𝑢 ↔ 𝑡 ∈ 𝑤))
Theorem	subelofd-P5.CL 643	Closed Form of subelofd-P5 642.
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 ∈ 𝑢 ↔ 𝑡 ∈ 𝑤))
6.3.2.3  Substitution Laws for Functions.
Theorem	subsucc-P5 644	Substitution Law for 's‘'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → s‘𝑡 = s‘𝑢)
Theorem	subaddl-P5 645	Left Substitution Law for '+'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 + 𝑤) = (𝑢 + 𝑤))
Theorem	subaddr-P5 646	Right Substitution Law for '+'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 + 𝑡) = (𝑤 + 𝑢))
Theorem	subaddd-P5 647	Dual Substitution Law for '+'.
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 + 𝑢) = (𝑡 + 𝑤))
Theorem	subaddd-P5.CL 648	Closed Form of subaddd-P5 647.
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 + 𝑢) = (𝑡 + 𝑤))
Theorem	submultl-P5 649	Left Substitution Law for '⋅'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤))
Theorem	submultr-P5 650	Right Substitution Law for '⋅'.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 ⋅ 𝑡) = (𝑤 ⋅ 𝑢))
Theorem	submultd-P5 651	Dual Substitution Law for '⋅'.
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 ⋅ 𝑢) = (𝑡 ⋅ 𝑤))
Theorem	submultd-P5.CL 652	Closed Form of submultd-P5 651.
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 ⋅ 𝑢) = (𝑡 ⋅ 𝑤))
6.4  Implicit Variable Substitution and Law of Specialization.
6.4.1  Preliminary Law of Specialization.
Theorem	lemma-L5.02a 653*	A lemma used for bound variable substitution and specialization theorems. '𝑥' cannot occur in either '𝑡' or '𝜓'. The '→' in the hypothesis is replaced with a '↔' in specisub-P5 654 to make the practical usage more clear.
⊢ (𝑥 = 𝑡 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	specisub-P5 654*	Specialization Theorem with Implicit Substitution. '𝑥' cannot occur in either '𝑡' or '𝜓'. The hypothesis is fulfilled when every free occurence of '𝑥' in '𝜑' is replaced with the term '𝑡', and every bound occurence of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'. After this operation, '𝑥' will not occur in '𝜓'. '𝑥' cannot occur in '𝑡' either, or it would occur in '𝜓' wherever '𝑥' was replaced.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	exiisub-P5 655*	Existential Quantifier Introduction Law with Implicit Substitution. '𝑥' cannot occur in either '𝑡' or '𝜓'. This is the dual of specisub-P5 654. The hypothesis is fulfilled when every free occurence of '𝑥' in '𝜑' is replaced with the term '𝑡', and every bound occurence of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'. '𝑥' cannot occur in '𝑡' either, or it would occur in '𝜓' wherever '𝑥' was replaced.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥𝜑)
6.4.2  Quantifier Removal Laws.
Theorem	qremallv-P5 656*	Universal Quantifier Removal (variable restriction). '𝑥' cannot occur in '𝜑'. The most general form is qremall-P6 722.
⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	qremexv-P5 657*	Existential Quantifier Removal (variable restriction). '𝑥' cannot occur in '𝜑'. The most general form is qremex-P6 723.
⊢ (∃𝑥𝜑 ↔ 𝜑)
6.4.3  Change of Bound Variables Laws.
Theorem	cbvallv-P5-L1 658*	Lemma for cbvallv-P5 659. [Auxiliary lemma - not displayed.]
Theorem	cbvallv-P5 659*	Change of Bound Variable Law for '∀𝑥' (variable restriction). '𝑥' cannot occur in '𝜓' and '𝑦' cannot occur in '𝜑'. The hypothesis is fulfilled when every free occurrence of '𝑥' in '𝜑' is replaced with '𝑦', and every bound occurance of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'. The most general form is cbvall-P6 751.
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexv-P5 660*	Change of Bound Variable Law for '∃𝑥' (variable restriction). '𝑥' cannot occur in '𝜓' and '𝑦' cannot occur in '𝜑'. The hypothesis is fulfilled when every free occurrence of '𝑥' in '𝜑' is replaced with '𝑦', and every bound occurance of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'. The most general form is cbvex-P6 752.
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
6.4.4  Weakened Law of Specialization.
Theorem	specw-P5 661*	Weak Version of Law of Specialization. Note that the hypothesis only requires the existence of a dummy variable '𝑥₁' and dummy formula '𝜑₁', that is equivalent to '𝜑' with free occurences of '𝑥' replaced with '𝑥₁' and bound occurances of '𝑥' replaced with fresh variables. Using induction on formula length, one can prove a meta-theorem stating that such a formula always exists. The building blocks of the inductive proof are the substitution theorems (theorems beginning with "sub") and the two bound variable replacement theorems (cbvallv-P5 659 and cbvexv-P5 660). Because meta-theorems don't exist in metamath, we will need the auxiliary "scheme completeness" axiom ax-L12 29 to eliminate the hypothesis in the general case (see spec-P6 719).
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	exiw-P5 662*	Weak Version of Existential Quantifier Introduction Law. This is the dual form of specw-P5 661. Note that the hypothesis only requires the existence of a dummy variable '𝑥₁' and dummy formula '𝜑₁', that is equivalent to '𝜑' with free occurences of '𝑥' replaced with '𝑥₁' and bound occurances of '𝑥' replaced with fresh variables. We will need the auxiliary "scheme completeness" axiom ax-L12 29 to eliminate the hypothesis in the general case (see exi-P6 718).
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
6.4.4.1  Hypothesis Elimination Examples.
Theorem	example-E5.01a 663*	Hypothesis Elimination Example 1.
⊢ (𝑥 = 𝑥₁ → ((𝑡 ⋅ (𝑢 + 𝑥)) = ((𝑡 ⋅ 𝑢) + (𝑡 ⋅ 𝑥)) ↔ (𝑡 ⋅ (𝑢 + 𝑥₁)) = ((𝑡 ⋅ 𝑢) + (𝑡 ⋅ 𝑥₁))))
Theorem	example-E5.02a 664*	Hypothesis Elimination Example 2.
⊢ (𝑥 = 𝑥₁ → (∀𝑦∃𝑧((𝑦 + 𝑧) = 𝑥 ∨ (𝑥 + 𝑧) = 𝑦) ↔ ∀𝑦∃𝑧((𝑦 + 𝑧) = 𝑥₁ ∨ (𝑥₁ + 𝑧) = 𝑦)))
Theorem	example-E5.03a 665*	Hypothesis Elimination Example 3.
⊢ (𝑥 = 𝑥₁ → (∀𝑧(𝑧 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ 𝑥₁ ↔ ∀𝑎(𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦))))
6.4.5  Commutivity of Similar Quantifiers (weakened versions).
Theorem	lemma-L5.03a 666*	A Lemma for Universal / Existential Conversion of Nested Quantifiers.
⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∃𝑥∃𝑦𝜑)
Theorem	lemma-L5.04a 667*	A lemma for commuting universal quantifiers. Requires the existence of '𝜑₁(𝑦₁)' as a replacement for '𝜑(𝑦)'.
⊢ (𝑦 = 𝑦₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	lemma-L5.05a 668*	A lemma for commuting existential quantifiers. Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	allcommw-P5 669*	Universal Quantifier Commutivity (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)', and the existance of '𝜑₂(𝑦₁)' as a replacement for '𝜑(𝑦)'. The form not requiring any hypotheses, but relying on an additional axiom is allcomm-P6 739.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ (𝑦 = 𝑦₁ → (𝜑 ↔ 𝜑₂))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excommw-P5 670*	Existential Quantifier Commutivity (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)', and the existance of '𝜑₂(𝑦₁)' as a replacement for '𝜑(𝑦)'. The form not requiring any hypotheses, but relying on an additional axiom is excomm-P6 740.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ (𝑦 = 𝑦₁ → (𝜑 ↔ 𝜑₂))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
6.5  Quantifier Collection Laws. The next four laws are useful for putting a WFF in prenex form. In this form all quantifiers are on the left and no logical connectives appear outside the scope of any individual quantifier. An example is given below.
Theorem	qcallimrv-P5 671*	Quantifier Collection Law: Universal Quantifier Right on Implication. (variable restriction). '𝑥' cannot occur in '𝜑'. The most general form is qcallimr-P6 757.
⊢ ((𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	qceximrv-P5 672*	Quantifier Collection Law: Existential Quantifier Right on Implication (variable restriction). '𝑥' cannot occur in '𝜑'. The most general form is qceximr-P6 758.
⊢ ((𝜑 → ∃𝑥𝜓) ↔ ∃𝑥(𝜑 → 𝜓))
Theorem	qcallimlv-P5 673*	Quantifier Collection Law: Universal Quantifier Left on Implication (variable restriction). '𝑥' cannot occur in '𝜓'. The most general form is qcalliml-P6 759.
⊢ ((∀𝑥𝜑 → 𝜓) ↔ ∃𝑥(𝜑 → 𝜓))
Theorem	qceximlv-P5 674*	Quantifier Collection Law: Existential Quantifier Left on Implication (variable restriction). '𝑥' cannot occur in '𝜓'. The most general form is qceximl-P6 760.
⊢ ((∃𝑥𝜑 → 𝜓) ↔ ∀𝑥(𝜑 → 𝜓))
6.5.0.1  Prenex Form Example.
Theorem	example-E5.04a 675*	Convert Axiom of Replacement to Prenex Form. The hypothesis imples we can construct an alternate function, '𝜑₂'. We first replace '𝑥' with '𝑥₁' in '𝜑' to obtain '𝜑₁', then we replace '𝑦' with '𝑦₁' in '𝜑₁' to obtain '𝜑₂'. Since '𝑥₁' and '𝑦₁' are fresh variables replacing '𝑥' and '𝑦', we need the disjoint variable conditions... $d 𝜑 𝑥₁ 𝑦₁ $. $d 𝜑₁ 𝑥 𝑦₁ $. $d 𝜑₂ 𝑥 𝑦 $. The other condition, that neither '𝑧' nor '𝑎' should appear in '𝜑' (and by extension '𝜑₁' and '𝜑₂'), is simply part of the hypothesis for with this version of the Axiom of Replacement.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ (𝑦 = 𝑦₁ → (𝜑₁ ↔ 𝜑₂))    &   ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑎∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))    ⇒   ⊢ ∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
PART 7  Chapter 6: Predicate Calculus (Definitions and ax-L10 - ax-L12).
7.1  Effective Non-Freeness.
7.1.1  The "General For" Concept. If a WFF '𝜑' satisfies the formula of ax-L5 17 with regard to some variable '𝑥', we say '𝜑' is *general for* '𝑥'.
7.1.1.1  Positive.
Theorem	genallw-P6 676*	The WFF ∀𝑥𝜑 is General for '𝑥' (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	genexw-P6 677*	The WFF ∃𝑥𝜑 is General for '𝑥' (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
7.1.1.2  Negated.
Theorem	gennallw-P6 678*	The WFF '¬ ∀𝑥𝜑' is General for '𝑥' (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	gennexw-P6 679*	The WFF '¬ ∃𝑥𝜑' is General for '𝑥' (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (¬ ∃𝑥𝜑 → ∀𝑥 ¬ ∃𝑥𝜑)
7.1.1.3  Dual.
Theorem	exgenallw-P6 680*	Dual of gennallw-P6 678 (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ (∃𝑥∀𝑥𝜑 → ∀𝑥𝜑)
7.1.2  Define Effective Non-Freeness.
7.1.2.1  Syntax Definition.
Syntax	wff-nfree 681	Extend WFF definition to include the effective non-freeness predicate 'Ⅎ'.
wff Ⅎ𝑥𝜑
7.1.2.2  Formal Definition.
Definition	df-nfree-D6.1 682	Definition of Effective Non-Freeness (ENF), 'Ⅎ'. Read as "is not (effectively) free in". When we say that '𝑥' is not (effectively) free in '𝜑', we are saying (in semantic terms) that the truth value of '𝜑' does not depend on '𝑥'. It is easy to understand this definition if we interpret the WFF '𝜑' as a function with a binary output. Then clearly '𝜑' does not depend on '𝑥' if and only if one of the following holds... 1. '𝜑' is true for all '𝑥' (holding all other variables constant). 2. '𝜑 is false for all '𝑥' (holding all other variables constant). This definition states exactly this. Unlike the regular textbook definition of non-freeness, it does *not* state that '𝑥' cannot occur free in '𝜑'. If we set '𝜑 ≔ 𝑥 = 𝑥' then '𝑥' is still *effectively* free in '𝜑' since '𝑥 = 𝑥' is a tautology in our system. Effective non-freeness is thus slightly more general than the standard textbook definition, which we will call grammatical non-freeness (GNF). We could also call effective non-freeness *logical* non-freenness because, unlike grammatical non-freeness, it is bound to logical equivalence (see nfrleq-P6 687).
⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))
7.1.3  Equivalencies. The laws nfrgenw-P6 684 and gennfrw-P6 685, show that *general for* and *effectively not free* are identical.
Theorem	dfnfreealt-P6 683	Alternate Definition of Effective Non-Freeness.
⊢ (Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	nfrgenw-P6 684*	ENF in ⇒ General for (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'. If '𝑥' is effectively not free in '𝜑', then '𝜑' is general for '𝑥'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	gennfrw-P6 685*	General for ⇒ ENF in (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'. If '𝜑' is general for '𝑥', then '𝑥' is effectively not free in '𝜑'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
7.1.4  Relationship to Textbook Definition. We define grammatical non-freeness (GNF) as follows... First, let '𝜑' be a well formed formula. We classify occurrences of the variable '𝑥' in '𝜑' as either *bound* or *free*. An occurrence of '𝑥' is *bound* if it appears inside a subformula of '𝜑' that has the form '∀𝑥𝜓' or '∃𝑥𝜓'. An occurrence of '𝑥' is *free* if it is not bound. A variable '𝑥' is (grammatically) *free in* a formula, '𝜑', if it occurs free in '𝜑'. Otherwise '𝑥' is said to be *not free in* '𝜑'. *Not free in* '𝜑' includes the case where '𝑥' appears nowhere in '𝜑'. Using the properties below, we can prove that if '𝑥' is gramatically not free (GNF) in '𝜑', then '𝑥' is also effectively not free (ENF) in '𝜑'. The converse is not always true though (consider the formula '𝑥 = 𝑥'). This means effective non-freeness is more general than grammatical non-freeness. Effective non-freeness is a more useful concept in the metamath language though, as it has the same meaning in all crucial cases and is defined logically rather than gramatically. We will now prove the statement... '𝑥 is GNF in 𝜑 ⇒ 𝑥 is ENF in 𝜑', for the case where '𝜑' is primitive (i.e. contains only '→', '¬', and '∀'). For the general case to follow, we need to impose an extra constraint on definitions (see *). ---------------------------------------------------------------------------- Proof: Base Case: Assume '𝜑' is atomic. Since an atomic formula cannot contain '∀𝑥', if '𝑥' occurs at all in '𝜑', it must occur free. Therefore if '𝑥' is GNF in '𝜑', then '𝑥' does not occur at all in '𝜑'. Therefore by nfrv-P6 686, '𝑥' is ENF in '𝜑'. Induction: Now assume the statement '𝑥 is GNF in 𝜑 ⇒ 𝑥 is ENF in 𝜑' is true for all WFFs of length less than 'n' and let '𝜑' be an arbitrary WFF of length 'n'. '𝜑' could have four possible forms... Case 1: '𝜑 ≔ ¬ 𝜓'. Note that '𝑥' occurs free in '𝜑' if and only if '𝑥' occurs free in 𝜓. Therefore if '𝑥' is GNF in '𝜑', then it is GNF in '𝜓'. Since '𝜓' has length 'n-1', we know '𝑥' is ENF in '𝜓'. Therefore, by nfrneg-P6 688, '𝑥' is ENF in ¬ 𝜓, i.e. '𝑥' is ENF in '𝜑'. Case 2: '𝜑 ≔ 𝜓 → 𝜒'. Not that if '𝑥' occurs free in either '𝜓' or '𝜒', then it occurs free in '𝜑'. Therefore if '𝑥' is GNF in '𝜑', then it is GNF in both '𝜓' and '𝜒'. Since both '𝜓' and '𝜒' have a length that is less than 'n', we know '𝑥' is ENF in both '𝜓' and '𝜒'. Therefore, by nfrim-P6 689, '𝑥' is ENF in 𝜓 → 𝜒, i.e. '𝑥' is ENF in '𝜑'. Case 3: '𝜑 ≔ ∀𝑥𝜓'. In this case it is definite that '𝑥' is GNF in '𝜑'. By nfrall1w-P6 692, '𝑥' is also ENF in '𝜑'. Case 4: '𝜑 ≔ ∀𝑦𝜓 ('𝑦' is different from '𝑥'). '𝑥' occurs free in '𝜑' if and only if it occurs free in '𝜓'. Therefore if '𝑥' is GNF in '𝜑', then it is GNF in 𝜓. Since '𝜓' has length 'n-1', we know '𝑥' is ENF in '𝜓' Therefore by nfrall2w-P6 694, '𝑥' is ENF in '∀𝑦𝜓', i.e. '𝑥' is ENF in '𝜑' By induction, we conclude that the statement... '𝑥 is GNF in 𝜑 ⇒ 𝑥 is ENF in 𝜑', is true for '𝜑' of any length. QED ---------------------------------------------------------------------------- * In order to forbid definitions from "hiding" free variable occurrences, we require that any free variable occurring in the definiens also occur in the definiendum. As an example, we are not allowed to define '⊤' as '𝑥 = 𝑥' since '𝑥' occurs free in '𝑥 = 𝑥'. Note that '𝑥' is still *effectively* free in '𝑥 = 𝑥' (since we can easily prove '𝑥 = 𝑥 → ∀𝑥𝑥 = 𝑥'), thus the definition is still sound. If '𝑥' were not effectively free OTOH, the definition would not even be sound. Given the constraints explained in the paragraph above, the exact same gramatically free variables that appear in a WFF containing definitions must also appear in the logically equivalent primitive form. This means '𝑥' is GNF in a WFF containing definitions if and only if it is GNF in the logically equivalent primitive form of the WFF. nfrleq-P6 687 can be used to show similarly, that '𝑥' is ENF in a WFF containing definitions if and only if '𝑥' is ENF in the logically equivalent primitive form of the WFF.
Theorem	nfrv-P6 686*	Does Not Occur in ⇒ ENF in. If '𝑥' does not occur in '𝜑', then '𝑥' is effectively not free in '𝜑'.
⊢ Ⅎ𝑥𝜑
Theorem	nfrleq-P6 687	Effective Non-Freeness is Bound to Logical Equivalence .
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
Theorem	nfrneg-P6 688	ENF Over Negation.
⊢ (Ⅎ𝑥 ¬ 𝜑 ↔ Ⅎ𝑥𝜑)
Theorem	nfrim-P6 689	ENF Over Implication.
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfrand-P6 690	ENF Over Conjunction.
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	nfrbi-P6 691	ENF Over Equivalency.
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)
Theorem	nfrall1w-P6 692*	ENF Over Universal Quantifier (same variable - weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	nfrex1w-P6 693*	ENF Over Existential Quantifier (same variable - weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    ⇒   ⊢ Ⅎ𝑥∃𝑥𝜑
Theorem	nfrall2w-P6 694*	ENF Over Universal Quantifier (different variable - weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfrex2w-P6 695*	ENF Over Existential Quantifier (different variable - weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
7.1.5  More Consequences of Effective Non-Freeness.
Theorem	nfrexgenw-P6 696*	Dual Form of nfrgenw-P6 684 (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	exgennfrw-P6 697*	Dual Form of gennfrw-P6 685 (weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ (∃𝑥𝜑 → 𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	qimeqalla-P6-L1 698	Lemma for qimeqalla-P6 699. [Auxiliary lemma - not displayed.]
Theorem	qimeqalla-P6 699	Quantified Implication Equivalence Law ( U ↔ ( E → U ) ) (non-freeness condition a).
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qimeqallb-P6-L1 700	Lemma for qimeqallb-P6 701. [Auxiliary lemma - not displayed.]