![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfcleq | GIF version |
Description: The same as df-cleq 2182 with the hypothesis removed using the Axiom of Extensionality ax-ext 2171. (Contributed by NM, 15-Sep-1993.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2171 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) | |
2 | 1 | df-cleq 2182 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∀wal 1362 = wceq 1364 ∈ wcel 2160 |
This theorem was proved from axioms: ax-ext 2171 |
This theorem depends on definitions: df-cleq 2182 |
This theorem is referenced by: cvjust 2184 eqriv 2186 eqrdv 2187 eqcom 2191 eqeq1 2196 eleq2 2253 cleqh 2289 abbi 2303 nfeq 2340 nfeqd 2347 cleqf 2357 eqss 3185 ddifstab 3282 ssequn1 3320 eqv 3457 disj3 3490 undif4 3500 vnex 4149 inex1 4152 zfpair2 4228 sucel 4428 uniex2 4454 bj-vprc 15101 bdinex1 15104 bj-zfpair2 15115 bj-uniex2 15121 |
Copyright terms: Public domain | W3C validator |