New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > dfcleq | GIF version |
Description: The same as df-cleq 2346 with the hypothesis removed using the Axiom of Extensionality ax-ext 2334. (Contributed by NM, 15-Sep-1993.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2334 | . 2 ⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z) | |
2 | 1 | df-cleq 2346 | 1 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∀wal 1540 = wceq 1642 ∈ wcel 1710 |
This theorem was proved from axioms: ax-ext 2334 |
This theorem depends on definitions: df-cleq 2346 |
This theorem is referenced by: cvjust 2348 eqriv 2350 eqrdv 2351 eqcom 2355 eqeq1 2359 eleq2 2414 cleqh 2450 abbi 2463 nfeq 2496 nfeqd 2503 cleqf 2513 dfss2 3262 eqss 3287 ssequn1 3433 necompl 3544 eqv 3565 disj3 3595 undif4 3607 axprimlem1 4088 axprimlem2 4089 ninexg 4097 1cex 4142 pw111 4170 opkelimagekg 4271 xpkvexg 4285 p6exg 4290 dfaddc2 4381 nnsucelrlem1 4424 ltfinex 4464 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenodddisjlem1 4515 nnadjoinlem1 4519 dfop2lem1 4573 eqop 4611 setconslem2 4732 dfswap2 4741 brimage 5793 releqel 5807 releqmpt2 5809 qsexg 5982 |
Copyright terms: Public domain | W3C validator |