![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > eqrdv | Structured version GIF version |
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.) |
Ref | Expression |
---|---|
eqrdv.1 | ⊢ (φ → (x ∈ A ↔ x ∈ B)) |
Ref | Expression |
---|---|
eqrdv | ⊢ (φ → A = B) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqrdv.1 | . . 3 ⊢ (φ → (x ∈ A ↔ x ∈ B)) | |
2 | 1 | alrimiv 1737 | . 2 ⊢ (φ → ∀x(x ∈ A ↔ x ∈ B)) |
3 | dfcleq 2017 | . 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | |
4 | 2, 3 | sylibr 137 | 1 ⊢ (φ → A = B) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∀wal 1226 = wceq 1228 ∈ wcel 1375 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1316 ax-gen 1318 ax-17 1401 ax-ext 2005 |
This theorem depends on definitions: df-bi 110 df-cleq 2016 |
This theorem is referenced by: eqrdav 2022 csbcomg 2849 csbabg 2883 uneq1 3066 ineq1 3107 difin2 3175 difsn 3474 intmin4 3616 iunconstm 3638 iinconstm 3639 dfiun2g 3662 iindif2m 3697 iinin2m 3698 iunxsng 3705 iunpw 4159 opthprc 4316 inimasn 4666 dmsnopg 4717 dfco2a 4746 iotaeq 4800 fun11iun 5070 ssimaex 5157 unpreima 5215 respreima 5218 fconstfvm 5302 reldm 5732 rntpos 5791 frecsuclem3 5901 iserd 6038 erth 6055 |
Copyright terms: Public domain | W3C validator |