![]() |
Metamath
Proof Explorer Theorem List (p. 29 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | abbi 2801 | Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2805, proved from fewer axioms, and hence is independently named. (Contributed by BJ and WL and SN, 20-Aug-2023.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | abbidv 2802* | Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2172, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbii 2803 | Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 3-May-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} | ||
Theorem | abbid 2804 | Equivalent wff's yield equal class abstractions (deduction form, with nonfreeness hypothesis). (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) Avoid ax-10 2138 and ax-11 2155. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbib 2805 | Equal class abstractions require equivalent formulas, and conversely. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-8 2109 and df-clel 2811 (by avoiding use of cleqh 2864). (Revised by BJ, 23-Jun-2019.) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | cbvabv 2806* | Rule used to change bound variables, using implicit substitution. Version of cbvab 2809 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2155 and ax-13 2372. (Revised by Steven Nguyen, 4-Dec-2022.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvabw 2807* | Rule used to change bound variables, using implicit substitution. Version of cbvab 2809 with a disjoint variable condition, which does not require ax-10 2138, ax-13 2372. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvabwOLD 2808* | Obsolete version of cbvabw 2807 as of 23-May-2024. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvab 2809 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Usage of the weaker cbvabw 2807 and cbvabv 2806 are preferred. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | eqabbw 2810* | Version of eqabb 2874 using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝜓)) | ||
Definition | df-clel 2811* |
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 2811 an axiom. See also comments under df-clab 2711, df-cleq 2725, and eqabb 2874. Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3648, clel3g 3651, and clel4g 3653. 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 2711, df-cleq 2725, and df-clel 2811 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 2811. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.) |
⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) & ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | dfclel 2812* | Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.) |
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | elex2 2813* | If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) Avoid ax-9 2117, ax-ext 2704, df-clab 2711. (Revised by Wolf Lammen, 30-Nov-2024.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | issetlem 2814* | Lemma for elisset 2816 and isset 3488. (Contributed by NM, 26-May-1993.) Extract from the proof of isset 3488. (Revised by WL, 2-Feb-2025.) |
⊢ 𝑥 ∈ 𝑉 ⇒ ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | elissetv 2815* | An element of a class exists. Version of elisset 2816 with a disjoint variable condition on 𝑉, 𝑥, avoiding df-clab 2711. Prefer its use over elisset 2816 when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by BJ, 14-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | elisset 2816* | An element of a class exists. Use elissetv 2815 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 2817 |
Weaker version of eleq1 2822 (but more general than elequ1 2114) not
depending on ax-ext 2704 nor df-cleq 2725.
Note that this provides a proof of ax-8 2109 from Tarski's FOL and dfclel 2812 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 228), which shows that dfclel 2812 is too powerful to be used as a definition instead of df-clel 2811. (Contributed by BJ, 24-Jun-2019.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | ||
Theorem | eleq2w 2818 | Weaker version of eleq2 2823 (but more general than elequ2 2122) not depending on ax-ext 2704 nor df-cleq 2725. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) | ||
Theorem | eleq1d 2819 | Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2822. (Revised by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | ||
Theorem | eleq2d 2820 | 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 2821 | Alternate proof of eleq2d 2820, shorter at the expense of requiring ax-12 2172. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 20-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq1 2822 | Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | ||
Theorem | eleq2 2823 | Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq12 2824 | Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | ||
Theorem | eleq1i 2825 | Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) | ||
Theorem | eleq2i 2826 | Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵) | ||
Theorem | eleq12i 2827 | Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷) | ||
Theorem | eleq12d 2828 | Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | ||
Theorem | eleq1a 2829 | A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |
⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | eqeltri 2830 | Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eqeltrri 2831 | Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐵 ∈ 𝐶 | ||
Theorem | eleqtri 2832 | Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eleqtrri 2833 | Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eqeltrd 2834 | Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrd 2835 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐶) | ||
Theorem | eleqtrd 2836 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrd 2837 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrid 2838 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrid 2839 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrid 2840 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrid 2841 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrdi 2842 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrdi 2843 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrdi 2844 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrdi 2845 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | 3eltr3i 2846 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶 ∈ 𝐷 | ||
Theorem | 3eltr4i 2847 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶 ∈ 𝐷 | ||
Theorem | 3eltr3d 2848 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4d 2849 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr3g 2850 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4g 2851 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | eleq2s 2852 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝐴 ∈ 𝐵 → 𝜑) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 → 𝜑) | ||
Theorem | eqneltri 2853 | 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 2854 | 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 2855 | 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 2856 | 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 2857 | 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 2858 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | ||
Theorem | nelneq2 2859 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | ||
Theorem | eqsb1 2860* | Substitution for the left-hand side in an equality. Class version of equsb3 2102. (Contributed by Rodolfo Medina, 28-Apr-2010.) |
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) | ||
Theorem | clelsb1 2861* | Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2115). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | ||
Theorem | clelsb2 2862* | Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2124). (Contributed by Jim Kingdon, 22-Nov-2018.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦) | ||
Theorem | clelsb2OLD 2863* | Obsolete version of clelsb2 2862 as of 24-Nov-2024.) (Contributed by Jim Kingdon, 22-Nov-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦) | ||
Theorem | cleqh 2864* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq 2726. See also cleqf 2935. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2019.) Remove dependency on ax-13 2372. (Revised by BJ, 30-Nov-2020.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | hbxfreq 2865 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1828 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | hblem 2866* | 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 2372. See hblemg 2867 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) | ||
Theorem | hblemg 2867* | Change the free variable of a hypothesis builder. Usage of this theorem is discouraged because it depends on ax-13 2372. See hblem 2866 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by NM, 21-Jun-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) | ||
Theorem | eqabdv 2868* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2155. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | ||
Theorem | eqabcdv 2869* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) | ||
Theorem | eqabi 2870* | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2155. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ 𝐴 = {𝑥 ∣ 𝜑} | ||
Theorem | abid1 2871* |
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 2727. The proof does not rely on cvjust 2727, so cvjust 2727
could be proved as a special instance of it. Note however that abid1 2871
necessarily relies on df-clel 2811, whereas cvjust 2727 does not.
This theorem requires ax-ext 2704, df-clab 2711, df-cleq 2725, df-clel 2811, 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 1541, cab 2710, and statements corresponding to defined class constructors. Note on the simultaneous presence in set.mm of this abid1 2871 and its commuted form abid2 2872: 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 2761 (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 12275 versus 1p1e2 12337. We do not need 1p1e2 12337, 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 12355, 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 565 and anidm 566, 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 2871 and abid2 2872 are in set.mm. (Contributed by NM, 26-Dec-1993.) (Revised by BJ, 10-Nov-2020.) |
⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | abid2 2872* | A simplification of class abstraction. Commuted form of abid1 2871. See comments there. (Contributed by NM, 26-Dec-1993.) |
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | eqab 2873* | One direction of eqabb 2874 is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025.) |
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑) → 𝐴 = {𝑥 ∣ 𝜑}) | ||
Theorem | eqabb 2874* |
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 2805 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 4251 and cp 9886; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9885. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. Usage of eqabbw 2810 is preferred since it requires fewer axioms. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | eqabbOLD 2875* | Obsolete version of eqabb 2874 as of 12-Feb-2025. (Contributed by NM, 26-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | eqabcb 2876* | Equality of a class variable and a class abstraction. Commuted form of eqabb 2874. (Contributed by NM, 20-Aug-1993.) |
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴)) | ||
Theorem | eqabrd 2877 | Equality of a class variable and a class abstraction (deduction form of eqabb 2874). (Contributed by NM, 16-Nov-1995.) |
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) | ||
Theorem | eqabri 2878 | 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 2879 | 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 2880* | 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 2155, see sbc5ALT 3807 for more details. (Revised by SN, 2-Sep-2024.) |
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | clelabOLD 2881* | Obsolete version of clelab 2880 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 2882* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))) | ||
Theorem | sbab 2883* | 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 2884 | Extend wff definition to include the not-free predicate for classes. |
wff Ⅎ𝑥𝐴 | ||
Theorem | nfcjust 2885* | Justification theorem for df-nfc 2886. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) | ||
Definition | df-nfc 2886* | 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 1787 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfci 2887* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcii 2888* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcr 2889* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Drop ax-12 2172 but use ax-8 2109, df-clel 2811, and avoid a DV condition on 𝑦, 𝐴. (Revised by SN, 3-Jun-2024.) |
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcrALT 2890* | Alternate version of nfcr 2889. Avoids ax-8 2109 but uses ax-12 2172. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcri 2891* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2138, ax-11 2155. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2172 (adopting Wolf Lammen's 13-May-2023 proof). (Revised by SN, 3-Jun-2024.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfcd 2892* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfcrd 2893* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcriOLD 2894* | Obsolete version of nfcri 2891 as of 3-Jun-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2138, ax-11 2155. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2172. (Revised by SN, 26-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfcriOLDOLD 2895* | Obsolete version of nfcri 2891 as of 26-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2138, ax-11 2155. (Revised by Gino Giotto, 23-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfcrii 2896* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2138, ax-11 2155. (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcriiOLD 2897* | Obsolete version of nfcrii 2896 as of 23-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcriOLDOLDOLD 2898* | Obsolete version of nfcri 2891 as of 23-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfceqdf 2899 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) Avoid ax-8 2109 and df-clel 2811. (Revised by WL and SN, 23-Aug-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) | ||
Theorem | nfceqdfOLD 2900 | Obsolete version of nfceqdf 2899 as of 23-Aug-2024. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |