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 1867 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | dfcleq 2164 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
4 | 2, 3 | sylibr 133 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1346 = wceq 1348 ∈ wcel 2141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: eqrdav 2169 csbcomg 3072 csbabg 3110 uneq1 3274 ineq1 3321 difin2 3389 difsn 3715 intmin4 3857 iunconstm 3879 iinconstm 3880 dfiun2g 3903 iindif2m 3938 iinin2m 3939 iunxsng 3946 iunxsngf 3948 iunpw 4463 opthprc 4660 inimasn 5026 dmsnopg 5080 dfco2a 5109 iotaeq 5166 fun11iun 5461 ssimaex 5555 unpreima 5618 respreima 5621 fconstfvm 5711 reldm 6162 rntpos 6233 frecsuclem 6382 iserd 6535 erth 6553 ecidg 6573 mapdm0 6637 map0e 6660 ixpiinm 6698 fifo 6953 ordiso2 7008 ctssdccl 7084 ctssdc 7086 genpassl 7473 genpassu 7474 1idprl 7539 1idpru 7540 sup3exmid 8860 eqreznegel 9560 iccid 9869 fzsplit2 9993 fzsn 10009 fzpr 10020 uzsplit 10035 fzoval 10091 frec2uzrand 10348 infssuzex 11891 mhmpropd 12676 discld 12889 restsn 12933 restdis 12937 cndis 12994 cnpdis 12995 tx1cn 13022 tx2cn 13023 blpnf 13153 blininf 13177 blres 13187 xmetec 13190 metrest 13259 xmetxpbl 13261 cnbl0 13287 reopnap 13291 bl2ioo 13295 cncfmet 13332 limcdifap 13384 |
Copyright terms: Public domain | W3C validator |