![]() |
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 1874 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfcleq 2171 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylibr 134 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 1447 ax-gen 1449 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: eqrdav 2176 csbcomg 3080 csbabg 3118 uneq1 3282 ineq1 3329 difin2 3397 difsn 3729 intmin4 3872 iunconstm 3894 iinconstm 3895 dfiun2g 3918 iindif2m 3953 iinin2m 3954 iunxsng 3961 iunxsngf 3963 iunpw 4479 opthprc 4676 inimasn 5045 dmsnopg 5099 dfco2a 5128 iotaeq 5185 fun11iun 5481 ssimaex 5576 unpreima 5640 respreima 5643 fconstfvm 5733 reldm 6184 rntpos 6255 frecsuclem 6404 iserd 6558 erth 6576 ecidg 6596 mapdm0 6660 map0e 6683 ixpiinm 6721 fifo 6976 ordiso2 7031 ctssdccl 7107 ctssdc 7109 exmidapne 7256 genpassl 7520 genpassu 7521 1idprl 7586 1idpru 7587 sup3exmid 8910 eqreznegel 9610 iccid 9921 fzsplit2 10045 fzsn 10061 fzpr 10072 uzsplit 10087 fzoval 10143 frec2uzrand 10400 infssuzex 11942 mhmpropd 12789 eqgid 13016 opprunitd 13210 unitpropdg 13248 subsubrg2 13305 subrgpropd 13307 discld 13507 restsn 13551 restdis 13555 cndis 13612 cnpdis 13613 tx1cn 13640 tx2cn 13641 blpnf 13771 blininf 13795 blres 13805 xmetec 13808 metrest 13877 xmetxpbl 13879 cnbl0 13905 reopnap 13909 bl2ioo 13913 cncfmet 13950 limcdifap 14002 |
Copyright terms: Public domain | W3C validator |