Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfcleq | Structured version Visualization version GIF version |
Description: The same as df-cleq 2603 with the hypothesis removed using the Axiom of Extensionality ax-ext 2590. (Contributed by NM, 15-Sep-1993.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2590 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) | |
2 | 1 | df-cleq 2603 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wal 1473 = wceq 1475 ∈ wcel 1977 |
This theorem was proved from axioms: ax-ext 2590 |
This theorem depends on definitions: df-cleq 2603 |
This theorem is referenced by: cvjust 2605 eqriv 2607 eqrdv 2608 eqeq1d 2612 eqeq1dALT 2613 eleq2d 2673 eleq2dOLD 2674 eleq2dALT 2675 cleqh 2711 nfeqd 2758 eqss 3583 ssequn1 3745 disj3 3973 undif4 3987 vprc 4724 inex1 4727 axpr 4832 zfpair2 4834 sucel 5715 uniex2 6850 nbcusgra 25992 cusgrauvtxb 26024 bnj145OLD 30049 brtxpsd3 31173 hfext 31460 onsuct0 31610 bj-abbi 31963 eliminable2a 32034 eliminable2b 32035 eliminable2c 32036 bj-ax9 32083 bj-df-cleq 32085 bj-sbeq 32088 bj-sbceqgALT 32089 bj-snsetex 32144 bj-df-v 32207 cover2 32678 rp-fakeinunass 36880 intimag 36967 relexp0eq 37012 ntrneik4w 37418 undif3VD 38140 dfcleqf 38281 rnmptpr 38353 dvnmul 38833 dvnprodlem3 38838 sge00 39269 sge0resplit 39299 sge0fodjrnlem 39309 hspdifhsp 39506 smfresal 39673 |
Copyright terms: Public domain | W3C validator |