Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqrdv | Unicode 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 1830 | . 2 |
3 | dfcleq 2111 | . 2 | |
4 | 2, 3 | sylibr 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1314 wceq 1316 wcel 1465 |
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 1408 ax-gen 1410 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: eqrdav 2116 csbcomg 2996 csbabg 3031 uneq1 3193 ineq1 3240 difin2 3308 difsn 3627 intmin4 3769 iunconstm 3791 iinconstm 3792 dfiun2g 3815 iindif2m 3850 iinin2m 3851 iunxsng 3858 iunxsngf 3860 iunpw 4371 opthprc 4560 inimasn 4926 dmsnopg 4980 dfco2a 5009 iotaeq 5066 fun11iun 5356 ssimaex 5450 unpreima 5513 respreima 5516 fconstfvm 5606 reldm 6052 rntpos 6122 frecsuclem 6271 iserd 6423 erth 6441 ecidg 6461 mapdm0 6525 map0e 6548 ixpiinm 6586 fifo 6836 ordiso2 6888 ctssdccl 6964 ctssdc 6966 genpassl 7300 genpassu 7301 1idprl 7366 1idpru 7367 sup3exmid 8683 eqreznegel 9374 iccid 9676 fzsplit2 9798 fzsn 9814 fzpr 9825 uzsplit 9840 fzoval 9893 frec2uzrand 10146 infssuzex 11569 discld 12232 restsn 12276 restdis 12280 cndis 12337 cnpdis 12338 tx1cn 12365 tx2cn 12366 blpnf 12496 blininf 12520 blres 12530 xmetec 12533 metrest 12602 xmetxpbl 12604 cnbl0 12630 reopnap 12634 bl2ioo 12638 cncfmet 12675 limcdifap 12727 |
Copyright terms: Public domain | W3C validator |