![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfcleq | GIF version |
Description: The same as df-cleq 2033 with the hypothesis removed using the Axiom of Extensionality ax-ext 2022. (Contributed by NM, 15-Sep-1993.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2022 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) | |
2 | 1 | df-cleq 2033 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∀wal 1241 = wceq 1243 ∈ wcel 1393 |
This theorem was proved from axioms: ax-ext 2022 |
This theorem depends on definitions: df-cleq 2033 |
This theorem is referenced by: cvjust 2035 eqriv 2037 eqrdv 2038 eqcom 2042 eqeq1 2046 eleq2 2101 cleqh 2137 abbi 2151 nfeq 2185 nfeqd 2192 cleqf 2201 eqss 2960 ssequn1 3113 eqv 3240 disj3 3272 undif4 3284 vprc 3888 inex1 3891 zfpair2 3945 sucel 4147 uniex2 4173 bj-vprc 10016 bdinex1 10019 bj-zfpair2 10030 bj-uniex2 10036 |
Copyright terms: Public domain | W3C validator |