![]() |
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 1754 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfcleq 2034 |
. 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 1336 ax-gen 1338 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqrdav 2039 csbcomg 2873 csbabg 2907 uneq1 3090 ineq1 3131 difin2 3199 difsn 3501 intmin4 3643 iunconstm 3665 iinconstm 3666 dfiun2g 3689 iindif2m 3724 iinin2m 3725 iunxsng 3732 iunpw 4211 opthprc 4391 inimasn 4741 dmsnopg 4792 dfco2a 4821 iotaeq 4875 fun11iun 5147 ssimaex 5234 unpreima 5292 respreima 5295 fconstfvm 5379 reldm 5812 rntpos 5872 frecsuclem3 5990 iserd 6132 erth 6150 ecidg 6170 ordiso2 6357 genpassl 6622 genpassu 6623 1idprl 6688 1idpru 6689 eqreznegel 8549 iccid 8794 fzsplit2 8914 fzsn 8929 fzpr 8939 uzsplit 8954 fzoval 9005 frec2uzrand 9191 |
Copyright terms: Public domain | W3C validator |