![]() |
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 1813 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | dfcleq 2094 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
4 | 2, 3 | sylibr 133 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1297 = wceq 1299 ∈ wcel 1448 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-17 1474 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: eqrdav 2099 csbcomg 2976 csbabg 3011 uneq1 3170 ineq1 3217 difin2 3285 difsn 3604 intmin4 3746 iunconstm 3768 iinconstm 3769 dfiun2g 3792 iindif2m 3827 iinin2m 3828 iunxsng 3835 iunxsngf 3837 iunpw 4339 opthprc 4528 inimasn 4892 dmsnopg 4946 dfco2a 4975 iotaeq 5032 fun11iun 5322 ssimaex 5414 unpreima 5477 respreima 5480 fconstfvm 5570 reldm 6014 rntpos 6084 frecsuclem 6233 iserd 6385 erth 6403 ecidg 6423 mapdm0 6487 map0e 6510 ixpiinm 6548 ordiso2 6835 ctssdclemr 6911 ctssdc 6912 genpassl 7233 genpassu 7234 1idprl 7299 1idpru 7300 sup3exmid 8573 eqreznegel 9256 iccid 9549 fzsplit2 9671 fzsn 9687 fzpr 9698 uzsplit 9713 fzoval 9766 frec2uzrand 10019 infssuzex 11437 discld 12087 restsn 12131 restdis 12135 cndis 12191 cnpdis 12192 tx1cn 12219 tx2cn 12220 blpnf 12328 blininf 12352 blres 12362 xmetec 12365 metrest 12434 cnbl0 12456 bl2ioo 12461 cncfmet 12492 limcdifap 12512 |
Copyright terms: Public domain | W3C validator |