![]() |
Metamath
Proof Explorer Theorem List (p. 29 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqeq1dALT 2801 | Shorter proof of eqeq1d 2800 based on more axioms. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 19-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | ||
Theorem | eqeq1 2802 | Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | ||
Theorem | eqeq1i 2803 | Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) | ||
Theorem | eqcomd 2804 | Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) Allow shortening of eqcom 2805. (Revised by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 = 𝐴) | ||
Theorem | eqcom 2805 | Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | ||
Theorem | eqcoms 2806 | Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.) |
⊢ (𝐴 = 𝐵 → 𝜑) ⇒ ⊢ (𝐵 = 𝐴 → 𝜑) | ||
Theorem | eqcomi 2807 | Inference from commutative law for class equality. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 = 𝐴 | ||
Theorem | neqcomd 2808 | Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 = 𝐴) | ||
Theorem | eqeq2d 2809 | Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Allow shortening of eqeq2 2810. (Revised by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | ||
Theorem | eqeq2 2810 | Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | ||
Theorem | eqeq2i 2811 | Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵) | ||
Theorem | eqeq12 2812 | Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | eqeq12i 2813 | A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) | ||
Theorem | eqeq12d 2814 | A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | eqeqan12d 2815 | A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2816. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | eqeqan12dALT 2816 | Alternate proof of eqeqan12d 2815. This proof has one more step but one fewer essential step. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | eqeqan12rd 2817 | A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | eqtr 2818 | Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) | ||
Theorem | eqtr2 2819 | A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) | ||
Theorem | eqtr3 2820 | A transitive law for class equality. (Contributed by NM, 20-May-2005.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) | ||
Theorem | eqtri 2821 | An equality transitivity inference. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 = 𝐶 | ||
Theorem | eqtr2i 2822 | An equality transitivity inference. (Contributed by NM, 21-Feb-1995.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐶 = 𝐴 | ||
Theorem | eqtr3i 2823 | An equality transitivity inference. (Contributed by NM, 6-May-1994.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 = 𝐶 ⇒ ⊢ 𝐵 = 𝐶 | ||
Theorem | eqtr4i 2824 | An equality transitivity inference. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 = 𝐶 | ||
Theorem | 3eqtri 2825 | An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 = 𝐶 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ 𝐴 = 𝐷 | ||
Theorem | 3eqtrri 2826 | An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 = 𝐶 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ 𝐷 = 𝐴 | ||
Theorem | 3eqtr2i 2827 | An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ 𝐴 = 𝐷 | ||
Theorem | 3eqtr2ri 2828 | An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ 𝐷 = 𝐴 | ||
Theorem | 3eqtr3i 2829 | An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶 = 𝐷 | ||
Theorem | 3eqtr3ri 2830 | An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐷 = 𝐶 | ||
Theorem | 3eqtr4i 2831 | An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶 = 𝐷 | ||
Theorem | 3eqtr4ri 2832 | An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐷 = 𝐶 | ||
Theorem | eqtrd 2833 | An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | eqtr2d 2834 | An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐶 = 𝐴) | ||
Theorem | eqtr3d 2835 | An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | eqtr4d 2836 | An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | 3eqtrd 2837 | A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐴 = 𝐷) | ||
Theorem | 3eqtrrd 2838 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 = 𝐴) | ||
Theorem | 3eqtr2d 2839 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐴 = 𝐷) | ||
Theorem | 3eqtr2rd 2840 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 = 𝐴) | ||
Theorem | 3eqtr3d 2841 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | 3eqtr3rd 2842 | A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 = 𝐶) | ||
Theorem | 3eqtr4d 2843 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | 3eqtr4rd 2844 | A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐷 = 𝐶) | ||
Theorem | syl5eq 2845 | An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | syl5req 2846 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐶 = 𝐴) | ||
Theorem | syl5eqr 2847 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | syl5reqr 2848 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐶 = 𝐴) | ||
Theorem | eqtrdi 2849 | An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | eqtr2di 2850 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐶 = 𝐴) | ||
Theorem | eqtr4di 2851 | An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | eqtr4id 2852 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | sylan9eq 2853 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐵 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) | ||
Theorem | sylan9req 2854 | An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ (𝜓 → 𝐵 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) | ||
Theorem | sylan9eqr 2855 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐵 = 𝐶) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶) | ||
Theorem | 3eqtr3g 2856 | A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | 3eqtr3a 2857 | A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | 3eqtr4g 2858 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | 3eqtr4a 2859 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | eq2tri 2860 | A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.) |
⊢ (𝐴 = 𝐶 → 𝐷 = 𝐹) & ⊢ (𝐵 = 𝐷 → 𝐶 = 𝐺) ⇒ ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐹) ↔ (𝐵 = 𝐷 ∧ 𝐴 = 𝐺)) | ||
Theorem | abbi1 2861 | Equivalent formulas yield equal class abstractions (closed form). This is the forward implication of abbi 2865, proved from fewer axioms. (Contributed by BJ and WL and SN, 20-Aug-2023.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | abbidv 2862* | Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2175, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbii 2863 | Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2142, ax-11 2158, and ax-12 2175. (Revised by Steven Nguyen, 3-May-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} | ||
Theorem | abbid 2864 | 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 2142 and ax-11 2158. (Revised by Wolf Lammen, 6-May-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbi 2865 | Equivalent formulas define equal class abstractions, and conversely. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-8 2113 and df-clel 2870 (by avoiding use of cleqh 2913). (Revised by BJ, 23-Jun-2019.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | cbvabv 2866* | Rule used to change bound variables, using implicit substitution. Version of cbvab 2869 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2158 and ax-13 2379. (Revised by Steven Nguyen, 4-Dec-2022.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvabw 2867* | Rule used to change bound variables, using implicit substitution. Version of cbvab 2869 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvabwOLD 2868* | Obsolete version of cbvabw 2867 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 2869 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Usage of the weaker cbvabw 2867 and cbvabv 2866 are preferred. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Definition | df-clel 2870* |
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 2870 an axiom. See also comments under df-clab 2777, df-cleq 2791, and abeq2 2922. Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2 3601, clel3 3603, and clel4 3604. 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 2777, df-cleq 2791, and df-clel 2870 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 2870. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.) |
⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) & ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | dfclel 2871* | Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.) |
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | eleq1w 2872 |
Weaker version of eleq1 2877 (but more general than elequ1 2118) not
depending on ax-ext 2770 nor df-cleq 2791.
Note that this provides a proof of ax-8 2113 from Tarski's FOL and dfclel 2871 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 232), which shows that dfclel 2871 is too powerful to be used as a definition instead of df-clel 2870. (Contributed by BJ, 24-Jun-2019.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | ||
Theorem | eleq2w 2873 | Weaker version of eleq2 2878 (but more general than elequ2 2126) not depending on ax-ext 2770 nor df-cleq 2791. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) | ||
Theorem | eleq1d 2874 | Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2877. (Revised by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | ||
Theorem | eleq2d 2875 | 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 2876 | Alternate proof of eleq2d 2875, shorter at the expense of requiring ax-12 2175. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 20-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq1 2877 | Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | ||
Theorem | eleq2 2878 | Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | ||
Theorem | eleq12 2879 | Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | ||
Theorem | eleq1i 2880 | Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) | ||
Theorem | eleq2i 2881 | Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵) | ||
Theorem | eleq12i 2882 | Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷) | ||
Theorem | eqneltri 2883 | 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 | eleq12d 2884 | Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | ||
Theorem | eleq1a 2885 | A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |
⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | eqeltri 2886 | Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eqeltrri 2887 | Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐵 ∈ 𝐶 | ||
Theorem | eleqtri 2888 | Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eleqtrri 2889 | Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ∈ 𝐶 | ||
Theorem | eqeltrd 2890 | Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrd 2891 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐶) | ||
Theorem | eleqtrd 2892 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrd 2893 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrid 2894 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrid 2895 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrid 2896 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrid 2897 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrdi 2898 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrdi 2899 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrdi 2900 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |