![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqrdv | GIF version |
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.) |
Ref | Expression |
---|---|
eqrdv.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
Ref | Expression |
---|---|
eqrdv | ⊢ (𝜑 → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqrdv.1 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | alrimiv 1796 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | dfcleq 2076 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
4 | 2, 3 | sylibr 132 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∀wal 1283 = wceq 1285 ∈ wcel 1434 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-17 1460 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-cleq 2075 |
This theorem is referenced by: eqrdav 2081 csbcomg 2930 csbabg 2964 uneq1 3120 ineq1 3167 difin2 3233 difsn 3531 intmin4 3672 iunconstm 3694 iinconstm 3695 dfiun2g 3718 iindif2m 3753 iinin2m 3754 iunxsng 3761 iunpw 4237 opthprc 4417 inimasn 4771 dmsnopg 4822 dfco2a 4851 iotaeq 4905 fun11iun 5178 ssimaex 5266 unpreima 5324 respreima 5327 fconstfvm 5411 reldm 5843 rntpos 5906 frecsuclem 6055 iserd 6198 erth 6216 ecidg 6236 ordiso2 6505 genpassl 6776 genpassu 6777 1idprl 6842 1idpru 6843 eqreznegel 8780 iccid 9024 fzsplit2 9145 fzsn 9160 fzpr 9170 uzsplit 9185 fzoval 9235 frec2uzrand 9487 infssuzex 10489 |
Copyright terms: Public domain | W3C validator |