![]() |
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 1751 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfcleq 2031 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylibr 137 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: eqrdav 2036 csbcomg 2867 csbabg 2901 uneq1 3084 ineq1 3125 difin2 3193 difsn 3492 intmin4 3634 iunconstm 3656 iinconstm 3657 dfiun2g 3680 iindif2m 3715 iinin2m 3716 iunxsng 3723 iunpw 4177 opthprc 4334 inimasn 4684 dmsnopg 4735 dfco2a 4764 iotaeq 4818 fun11iun 5090 ssimaex 5177 unpreima 5235 respreima 5238 fconstfvm 5322 reldm 5754 rntpos 5813 frecsuclem3 5929 iserd 6068 erth 6086 ecidg 6106 genpassl 6507 genpassu 6508 1idprl 6566 1idpru 6567 eqreznegel 8325 iccid 8564 fzsplit2 8684 fzsn 8699 fzpr 8709 uzsplit 8724 fzoval 8775 frec2uzrand 8872 |
Copyright terms: Public domain | W3C validator |