| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > eleq12d | Unicode version | ||
| Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
| Ref | Expression |
|---|---|
| eleq1d.1 |
|
| eleq12d.2 |
|
| Ref | Expression |
|---|---|
| eleq12d |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq12d.2 |
. . 3
| |
| 2 | 1 | eleq2d 2274 |
. 2
|
| 3 | eleq1d.1 |
. . 3
| |
| 4 | 3 | eleq1d 2273 |
. 2
|
| 5 | 2, 4 | bitrd 188 |
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 1469 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-4 1532 ax-17 1548 ax-ial 1556 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-cleq 2197 df-clel 2200 |
| This theorem is referenced by: cbvraldva2 2744 cbvrexdva2 2745 cdeqel 2993 ru 2996 sbceqbid 3004 sbcel12g 3107 cbvralcsf 3155 cbvrexcsf 3156 cbvreucsf 3157 cbvrabcsf 3158 onintexmid 4620 elvvuni 4738 elrnmpt1 4928 canth 5896 smoeq 6375 smores 6377 smores2 6379 iordsmo 6382 nnaordi 6593 nnaordr 6595 fvixp 6789 cbvixp 6801 mptelixpg 6820 opabfi 7034 exmidaclem 7319 cc1 7376 cc2lem 7377 cc3 7379 ltapig 7450 ltmpig 7451 fzsubel 10181 elfzp1b 10218 ennnfonelemg 12745 ennnfonelemp1 12748 ennnfonelemnn0 12764 ctiunctlemu1st 12776 ctiunctlemu2nd 12777 ctiunctlemudc 12779 ctiunctlemfo 12781 prdsbasprj 13085 xpsfrnel 13147 ismgm 13160 mgm1 13173 issgrpd 13215 ismndd 13240 eqgfval 13529 ringcl 13746 unitinvcl 13856 aprval 14015 aprap 14019 islmodd 14026 rspcl 14224 rnglidlmmgm 14229 zndvds 14382 istps 14475 tpspropd 14479 eltpsg 14483 isms 14896 mspropd 14921 cnlimci 15116 |
| Copyright terms: Public domain | W3C validator |