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 2708) and the definition of class equality (df-cleq 2729). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2711 to prove also the hypothesis of df-cleq 2729 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1803, equid 2020 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axextb 2711 | . 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧)) | |
2 | axextb 2711 | . 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡)) | |
3 | 1, 2 | df-cleq 2729 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∀wal 1541 = wceq 1543 ∈ wcel 2110 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-cleq 2729 |
This theorem is referenced by: cvjust 2731 ax9ALT 2732 eleq2w2 2733 eqriv 2734 eqrdv 2735 eqeq1d 2739 eqeq1dALT 2740 abbi 2810 abeq2w 2815 eleq2d 2823 eleq2dALT 2824 cleqh 2861 nfeqd 2914 cleqf 2935 raleqbidvv 3315 eqv 3417 abv 3419 csbied 3849 dfss2 3886 eqss 3916 ssequn1 4094 vn0 4253 eq0 4258 eq0ALT 4259 ab0w 4288 ab0OLD 4290 ab0orv 4293 eq0rdv 4319 disj 4362 disj3 4368 undif4 4381 rzal 4420 ralf0 4425 intprg 4892 vnex 5207 inex1 5210 axprALT 5315 zfpair2 5323 sucel 6286 uniex2 7526 brtxpsd3 33935 hfext 34222 onsuct0 34367 eliminable2a 34781 eliminable2b 34782 eliminable2c 34783 eliminable-veqab 34787 eliminable-abeqv 34788 eliminable-abeqab 34789 bj-sbeq 34823 bj-sbceqgALT 34824 bj-snsetex 34890 eleq2w2ALT 34957 cover2 35609 releccnveq 36134 rp-fakeinunass 40807 intimag 40941 relexp0eq 40986 ntrneik4w 41387 undif3VD 42175 uzinico 42773 dvnmul 43159 dvnprodlem3 43164 sge00 43589 sge0resplit 43619 sge0fodjrnlem 43629 hspdifhsp 43829 smfresal 43994 mo0sn 45834 |
Copyright terms: Public domain | W3C validator |