![]() |
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 2741 with the hypothesis removed using the Axiom of Extensionality ax-ext 2728. (Contributed by NM, 15-Sep-1993.) Revised to make use of axext3 2730 instead of ax-ext 2728, so that ax-9 2136 will appear in lists of axioms used by a proof, since df-cleq 2741 implies ax-9 2136 by theorem bj-ax9 33167. We may revisit this in the future. (Revised by NM, 28-Oct-2021.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axext3 2730 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) | |
2 | 1 | df-cleq 2741 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∀wal 1618 = wceq 1620 ∈ wcel 2127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1842 df-cleq 2741 |
This theorem is referenced by: cvjust 2743 eqriv 2745 eqrdv 2746 eqeq1d 2750 eqeq1dALT 2751 eleq2d 2813 eleq2dALT 2814 cleqh 2850 nfeqd 2898 eqss 3747 ssequn1 3914 disj3 4152 undif4 4167 vprc 4936 inex1 4939 axpr 5042 zfpair2 5044 sucel 5947 uniex2 7105 brtxpsd3 32280 hfext 32567 onsuct0 32717 bj-abbi 33052 eliminable2a 33118 eliminable2b 33119 eliminable2c 33120 bj-df-cleq 33170 bj-sbeq 33173 bj-sbceqgALT 33174 bj-snsetex 33228 bj-df-v 33293 cover2 33790 releccnveq 34315 rp-fakeinunass 38332 intimag 38419 relexp0eq 38464 ntrneik4w 38869 undif3VD 39586 rnmptpr 39826 uzinico 40259 dvnmul 40630 dvnprodlem3 40635 sge00 41065 sge0resplit 41095 sge0fodjrnlem 41105 hspdifhsp 41305 smfresal 41470 |
Copyright terms: Public domain | W3C validator |