Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfcleq | Structured version Visualization version GIF version |
Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2795) and the definition of class equality (df-cleq 2816). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2798 to prove also the hypothesis of df-cleq 2816 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1796, equid 2019 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axextb 2798 | . 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧)) | |
2 | axextb 2798 | . 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡)) | |
3 | 1, 2 | df-cleq 2816 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∀wal 1535 = wceq 1537 ∈ wcel 2114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2124 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2816 |
This theorem is referenced by: cvjust 2818 ax9ALT 2819 eqriv 2820 eqrdv 2821 eqeq1d 2825 eqeq1dALT 2826 abbi 2890 eleq2d 2900 eleq2dALT 2901 cleqh 2938 nfeqd 2990 cleqf 3012 eqv 3504 eqss 3984 ssequn1 4158 disj3 4405 undif4 4418 vnex 5220 inex1 5223 axprALT 5325 zfpair2 5333 sucel 6266 uniex2 7466 brtxpsd3 33359 hfext 33646 onsuct0 33791 eliminable2a 34185 eliminable2b 34186 eliminable2c 34187 bj-ax9 34218 bj-sbeq 34220 bj-sbceqgALT 34221 bj-snsetex 34277 bj-df-v 34349 cover2 34991 releccnveq 35521 rp-fakeinunass 39888 intimag 40008 relexp0eq 40053 ntrneik4w 40457 undif3VD 41223 uzinico 41843 dvnmul 42235 dvnprodlem3 42240 sge00 42665 sge0resplit 42695 sge0fodjrnlem 42705 hspdifhsp 42905 smfresal 43070 |
Copyright terms: Public domain | W3C validator |