![]() |
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 1884 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | dfcleq 2182 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
4 | 2, 3 | sylibr 134 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wal 1361 = wceq 1363 ∈ wcel 2159 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-gen 1459 ax-17 1536 ax-ext 2170 |
This theorem depends on definitions: df-bi 117 df-cleq 2181 |
This theorem is referenced by: eqrdav 2187 eqabdv 2317 csbcomg 3094 csbabg 3132 uneq1 3296 ineq1 3343 difin2 3411 difsn 3743 intmin4 3886 iunconstm 3908 iinconstm 3909 dfiun2g 3932 iindif2m 3968 iinin2m 3969 iunxsng 3976 iunxsngf 3978 iunpw 4494 opthprc 4691 inimasn 5060 dmsnopg 5114 dfco2a 5143 iotaeq 5200 fun11iun 5496 ssimaex 5592 unpreima 5656 respreima 5659 fconstfvm 5749 reldm 6204 rntpos 6275 frecsuclem 6424 iserd 6578 erth 6596 ecidg 6616 mapdm0 6680 map0e 6703 ixpiinm 6741 fifo 6996 ordiso2 7051 ctssdccl 7127 ctssdc 7129 exmidapne 7276 genpassl 7540 genpassu 7541 1idprl 7606 1idpru 7607 sup3exmid 8931 eqreznegel 9631 iccid 9942 fzsplit2 10067 fzsn 10083 fzpr 10094 uzsplit 10109 fzoval 10165 frec2uzrand 10422 infssuzex 11967 mhmpropd 12883 eqgid 13130 ghmmhmb 13153 ghmpropd 13182 ablnsg 13231 opprsubgg 13394 opprunitd 13420 unitpropdg 13458 opprsubrngg 13518 subsubrng2 13522 subrngpropd 13523 subsubrg2 13553 subrgpropd 13555 lssats2 13690 lsspropdg 13707 discld 14019 restsn 14063 restdis 14067 cndis 14124 cnpdis 14125 tx1cn 14152 tx2cn 14153 blpnf 14283 blininf 14307 blres 14317 xmetec 14320 metrest 14389 xmetxpbl 14391 cnbl0 14417 reopnap 14421 bl2ioo 14425 cncfmet 14462 limcdifap 14514 |
Copyright terms: Public domain | W3C validator |