| 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 1795, equid 2011 }. (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 206 ∀wal 1538 = wceq 1540 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: cvjust 2731 ax9ALT 2732 eleq2w2 2733 eqriv 2734 eqrdv 2735 eqeq1d 2739 eqeq1dALT 2740 abbib 2811 eqabbw 2815 eleq2d 2827 eleq2dALT 2828 cleqh 2871 nfeqd 2916 cleqf 2934 rexeq 3322 raleqbidvvOLD 3335 rmoeq1 3416 eqv 3490 abv 3492 csbied 3935 dfss2 3969 eqss 3999 ssequn1 4186 vn0 4345 eq0 4350 eq0ALT 4351 ab0w 4379 ab0orv 4383 eq0rdv 4407 disj 4450 disj3 4454 undif4 4467 rzal 4509 ralf0 4514 intprg 4981 vnex 5314 inex1 5317 axprALT 5422 zfpair2 5433 sucel 6458 uniex2 7758 brtxpsd3 35897 hfext 36184 in-ax8 36225 onsuct0 36442 eliminable2a 36861 eliminable2b 36862 eliminable2c 36863 eliminable-veqab 36867 eliminable-abeqv 36868 eliminable-abeqab 36869 bj-sbeq 36902 bj-sbceqgALT 36903 bj-snsetex 36964 bj-clex 37032 eleq2w2ALT 37048 wl-cleq-0 37496 wl-cleq-1 37497 wl-cleq-2 37498 wl-cleq-3 37499 wl-cleq-4 37500 wl-cleq-5 37501 wl-cleq-6 37502 cover2 37722 releccnveq 38259 abbibw 42687 rp-fakeinunass 43528 intimag 43669 relexp0eq 43714 ntrneik4w 44113 undif3VD 44902 uzinico 45573 dvnmul 45958 dvnprodlem3 45963 sge00 46391 sge0resplit 46421 sge0fodjrnlem 46431 hspdifhsp 46631 smfresal 46803 mo0sn 48735 |
| Copyright terms: Public domain | W3C validator |