![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfcleq | GIF version |
Description: The same as df-cleq 2093 with the hypothesis removed using the Axiom of Extensionality ax-ext 2082. (Contributed by NM, 15-Sep-1993.) |
Ref | Expression |
---|---|
dfcleq | ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2082 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) | |
2 | 1 | df-cleq 2093 | 1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∀wal 1297 = wceq 1299 ∈ wcel 1448 |
This theorem was proved from axioms: ax-ext 2082 |
This theorem depends on definitions: df-cleq 2093 |
This theorem is referenced by: cvjust 2095 eqriv 2097 eqrdv 2098 eqcom 2102 eqeq1 2106 eleq2 2163 cleqh 2199 abbi 2213 nfeq 2248 nfeqd 2255 cleqf 2264 eqss 3062 ddifstab 3155 ssequn1 3193 eqv 3329 disj3 3362 undif4 3372 vnex 3999 inex1 4002 zfpair2 4070 sucel 4270 uniex2 4296 bj-vprc 12675 bdinex1 12678 bj-zfpair2 12689 bj-uniex2 12695 |
Copyright terms: Public domain | W3C validator |