![]() |
Metamath
Proof Explorer Theorem List (p. 29 of 485) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqabbw 2801* | Version of eqabb 2865 using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝜓)) | ||
Definition | df-clel 2802* |
Define the membership connective between classes. Theorem 6.3 of
[Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we
adopt as a definition. See these references for its metalogical
justification.
The hypotheses express that all instances of the conclusion where class variables are replaced with setvar variables hold. Therefore, this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This is only a proof sketch of conservativity; for details see Appendix of [Levy] p. 357. This is the reason why we call this axiomatic statement a "definition", even though it does not have the usual form of a definition. If we required a definition to have the usual form, we would call df-clel 2802 an axiom. See also comments under df-clab 2703, df-cleq 2717, and eqabb 2865. Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3642, clel3g 3645, and clel4g 3647. This is called the "axiom of membership" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. While the three class definitions df-clab 2703, df-cleq 2717, and df-clel 2802 are eliminable and conservative and thus meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the requirements for the current definition checker. The proofs of conservativity require external justification that is beyond the scope of the definition checker. For a general discussion of the theory of classes, see mmset.html#class 2802. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.) |
⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) & ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | dfclel 2803* | Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.) |
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | elex2 2804* | If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) Avoid ax-9 2108, ax-ext 2696, df-clab 2703. (Revised by Wolf Lammen, 30-Nov-2024.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | issetlem 2805* | Lemma for elisset 2807 and isset 3474. (Contributed by NM, 26-May-1993.) Extract from the proof of isset 3474. (Revised by WL, 2-Feb-2025.) |
⊢ 𝑥 ∈ 𝑉 ⇒ ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | elissetv 2806* | An element of a class exists. Version of elisset 2807 with a disjoint variable condition on 𝑉, 𝑥, avoiding df-clab 2703. Prefer its use over elisset 2807 when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by BJ, 14-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | elisset 2807* | An element of a class exists. Use elissetv 2806 instead when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by NM, 1-May-1995.) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | eleq1w 2808 |
Weaker version of eleq1 2813 (but more general than elequ1 2105) not
depending on ax-ext 2696 nor df-cleq 2717.
Note that this provides a proof of ax-8 2100 from Tarski's FOL and dfclel 2803 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 228), which shows that dfclel 2803 is too powerful to be used as a definition instead of df-clel 2802. (Contributed by BJ, 24-Jun-2019.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | ||
Theorem | eleq2w 2809 | Weaker version of eleq2 2814 (but more general than elequ2 2113) not depending on ax-ext 2696 nor df-cleq 2717. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) | ||
Theorem | eleq1d 2810 | Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2813. (Revised by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | ||
Theorem | eleq2d 2811 | Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq2dALT 2812 | Alternate proof of eleq2d 2811, shorter at the expense of requiring ax-12 2166. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 20-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq1 2813 | Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | ||
Theorem | eleq2 2814 | Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq12 2815 | Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | ||
Theorem | eleq1i 2816 | Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) | ||
Theorem | eleq2i 2817 | Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵) | ||
Theorem | eleq12i 2818 | Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷) | ||
Theorem | eleq12d 2819 | Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | ||
Theorem | eleq1a 2820 | A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |
⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | eqeltri 2821 | Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eqeltrri 2822 | Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐵 ∈ 𝐶 | ||
Theorem | eleqtri 2823 | Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eleqtrri 2824 | Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eqeltrd 2825 | Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrd 2826 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐶) | ||
Theorem | eleqtrd 2827 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrd 2828 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrid 2829 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrid 2830 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrid 2831 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrid 2832 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrdi 2833 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrdi 2834 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrdi 2835 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrdi 2836 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | 3eltr3i 2837 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶 ∈ 𝐷 | ||
Theorem | 3eltr4i 2838 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶 ∈ 𝐷 | ||
Theorem | 3eltr3d 2839 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4d 2840 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr3g 2841 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4g 2842 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | eleq2s 2843 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝐴 ∈ 𝐵 → 𝜑) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 → 𝜑) | ||
Theorem | eqneltri 2844 | If a class is not an element of another class, an equal class is also not an element. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝐴 = 𝐵 & ⊢ ¬ 𝐵 ∈ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ 𝐶 | ||
Theorem | eqneltrd 2845 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | eqneltrrd 2846 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 13-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) | ||
Theorem | neleqtrd 2847 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | neleqtrrd 2848 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 13-Nov-2019.) |
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) | ||
Theorem | nelneq 2849 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | ||
Theorem | nelneq2 2850 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | ||
Theorem | eqsb1 2851* | Substitution for the left-hand side in an equality. Class version of equsb3 2093. (Contributed by Rodolfo Medina, 28-Apr-2010.) |
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) | ||
Theorem | clelsb1 2852* | Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2106). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | ||
Theorem | clelsb2 2853* | Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2115). (Contributed by Jim Kingdon, 22-Nov-2018.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦) | ||
Theorem | clelsb2OLD 2854* | Obsolete version of clelsb2 2853 as of 24-Nov-2024.) (Contributed by Jim Kingdon, 22-Nov-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦) | ||
Theorem | cleqh 2855* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq 2718. See also cleqf 2923. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2019.) Remove dependency on ax-13 2365. (Revised by BJ, 30-Nov-2020.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | hbxfreq 2856 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1819 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | hblem 2857* | Change the free variable of a hypothesis builder. (Contributed by NM, 21-Jun-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) Add disjoint variable condition to avoid ax-13 2365. See hblemg 2858 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) | ||
Theorem | hblemg 2858* | Change the free variable of a hypothesis builder. Usage of this theorem is discouraged because it depends on ax-13 2365. See hblem 2857 for a version with more disjoint variable conditions, but not requiring ax-13 2365. (Contributed by NM, 21-Jun-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) | ||
Theorem | eqabdv 2859* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2146. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | ||
Theorem | eqabcdv 2860* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) | ||
Theorem | eqabi 2861* | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2146. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ 𝐴 = {𝑥 ∣ 𝜑} | ||
Theorem | abid1 2862* |
Every class is equal to a class abstraction (the class of sets belonging
to it). Theorem 5.2 of [Quine] p. 35.
This is a generalization to
classes of cvjust 2719. The proof does not rely on cvjust 2719, so cvjust 2719
could be proved as a special instance of it. Note however that abid1 2862
necessarily relies on df-clel 2802, whereas cvjust 2719 does not.
This theorem requires ax-ext 2696, df-clab 2703, df-cleq 2717, df-clel 2802, but to prove that any specific class term not containing class variables is a setvar or is equal to a class abstraction does not require these $a-statements. This last fact is a metatheorem, consequence of the fact that the only $a-statements with typecode class are cv 1532, cab 2702, and statements corresponding to defined class constructors. Note on the simultaneous presence in set.mm of this abid1 2862 and its commuted form abid2 2863: It is rare that two forms so closely related both appear in set.mm. Indeed, such equalities are generally used in later proofs as parts of transitive inferences, and with the many variants of eqtri 2753 (search for *eqtr*), it would be rare that either one would shorten a proof compared to the other. There is typically a choice between what we call a "definitional form", where the shorter expression is on the LHS (left-hand side), and a "computational form", where the shorter expression is on the RHS (right-hand side). An example is df-2 12308 versus 1p1e2 12370. We do not need 1p1e2 12370, but because it occurs "naturally" in computations, it can be useful to have it directly, together with a uniform set of 1-digit operations like 1p2e3 12388, etc. In most cases, we do not need both a definitional and a computational forms. A definitional form would favor consistency with genuine definitions, while a computational form is often more natural. The situation is similar with biconditionals in propositional calculus: see for instance pm4.24 562 and anidm 563, while other biconditionals generally appear in a single form (either definitional, but more often computational). In the present case, the equality is important enough that both abid1 2862 and abid2 2863 are in set.mm. (Contributed by NM, 26-Dec-1993.) (Revised by BJ, 10-Nov-2020.) |
⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | abid2 2863* | A simplification of class abstraction. Commuted form of abid1 2862. See comments there. (Contributed by NM, 26-Dec-1993.) |
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | eqab 2864* | One direction of eqabb 2865 is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025.) |
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑) → 𝐴 = {𝑥 ∣ 𝜑}) | ||
Theorem | eqabb 2865* |
Equality of a class variable and a class abstraction (also called a
class builder). Theorem 5.1 of [Quine]
p. 34. This theorem shows the
relationship between expressions with class abstractions and expressions
with class variables. Note that abbib 2797 and its relatives are among
those useful for converting theorems with class variables to equivalent
theorems with wff variables, by first substituting a class abstraction
for each class variable.
Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥 ∈ 𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. An example is the conversion of zfauscl 5302 to inex1 5318 (look at the instance of zfauscl 5302 that occurs in the proof of inex1 5318). Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥 ∣ 𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new setvar and wff variables not already in the wff. Examples include dfsymdif2 4249 and cp 9916; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9915. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. Usage of eqabbw 2801 is preferred since it requires fewer axioms. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | eqabbOLD 2866* | Obsolete version of eqabb 2865 as of 12-Feb-2025. (Contributed by NM, 26-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | eqabcb 2867* | Equality of a class variable and a class abstraction. Commuted form of eqabb 2865. (Contributed by NM, 20-Aug-1993.) |
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴)) | ||
Theorem | eqabrd 2868 | Equality of a class variable and a class abstraction (deduction form of eqabb 2865). (Contributed by NM, 16-Nov-1995.) |
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) | ||
Theorem | eqabri 2869 | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | ||
Theorem | eqabcri 2870 | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Nov-2019.) |
⊢ {𝑥 ∣ 𝜑} = 𝐴 ⇒ ⊢ (𝜑 ↔ 𝑥 ∈ 𝐴) | ||
Theorem | clelab 2871* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) Avoid ax-11 2146, see sbc5ALT 3802 for more details. (Revised by SN, 2-Sep-2024.) |
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | clelabOLD 2872* | Obsolete version of clelab 2871 as of 2-Sep-2024. (Contributed by NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | clabel 2873* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))) | ||
Theorem | sbab 2874* | The right-hand side of the second equality is a way of representing proper substitution of 𝑦 for 𝑥 into a class variable. (Contributed by NM, 14-Sep-2003.) |
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴}) | ||
Syntax | wnfc 2875 | Extend wff definition to include the not-free predicate for classes. |
wff Ⅎ𝑥𝐴 | ||
Theorem | nfcjust 2876* | Justification theorem for df-nfc 2877. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) | ||
Definition | df-nfc 2877* | Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf 1778 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfci 2878* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcii 2879* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcr 2880* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Drop ax-12 2166 but use ax-8 2100, df-clel 2802, and avoid a DV condition on 𝑦, 𝐴. (Revised by SN, 3-Jun-2024.) |
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcrALT 2881* | Alternate version of nfcr 2880. Avoids ax-8 2100 but uses ax-12 2166. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcri 2882* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2129, ax-11 2146. (Revised by GG, 23-May-2024.) Avoid ax-12 2166 (adopting Wolf Lammen's 13-May-2023 proof). (Revised by SN, 3-Jun-2024.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfcd 2883* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfcrd 2884* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcrii 2885* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2129, ax-11 2146. (Revised by GG, 23-May-2024.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfceqdf 2886 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) Avoid ax-8 2100 and df-clel 2802. (Revised by WL and SN, 23-Aug-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) | ||
Theorem | nfceqdfOLD 2887 | Obsolete version of nfceqdf 2886 as of 23-Aug-2024. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) | ||
Theorem | nfceqi 2888 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) Avoid ax-12 2166. (Revised by Wolf Lammen, 19-Jun-2023.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) | ||
Theorem | nfcxfr 2889 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcxfrd 2890 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfcv 2891* | If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcvd 2892* | If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfab1 2893 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} | ||
Theorem | nfnfc1 2894 | The setvar 𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥Ⅎ𝑥𝐴 | ||
Theorem | clelsb1fw 2895* | Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2106). Version of clelsb1f 2896 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Rodolfo Medina, 28-Apr-2010.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | ||
Theorem | clelsb1f 2896 | Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2106). Usage of this theorem is discouraged because it depends on ax-13 2365. See clelsb1fw 2895 not requiring ax-13 2365, but extra disjoint variables. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) (Proof shortened by Wolf Lammen, 7-May-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | ||
Theorem | nfab 2897* | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2365. See nfabg 2898 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} | ||
Theorem | nfabg 2898 | Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2365. See nfab 2897 for a version with more disjoint variable conditions, but not requiring ax-13 2365. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} | ||
Theorem | nfaba1 2899* | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2365. See nfaba1g 2901 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) Avoid ax-6 1963, ax-7 2003, ax-12 2166. (Revised by SN, 14-May-2025.) |
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑} | ||
Theorem | nfaba1OLD 2900* | Obsolete version of nfaba1 2899 as of 14-May-2025. (Contributed by Mario Carneiro, 14-Oct-2016.) (Revised by GG, 20-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |