![]() |
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 2247 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eleq1d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | eleq1d 2246 |
. 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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: cbvraldva2 2710 cbvrexdva2 2711 cdeqel 2958 ru 2961 sbceqbid 2969 sbcel12g 3072 cbvralcsf 3119 cbvrexcsf 3120 cbvreucsf 3121 cbvrabcsf 3122 onintexmid 4572 elvvuni 4690 elrnmpt1 4878 canth 5828 smoeq 6290 smores 6292 smores2 6294 iordsmo 6297 nnaordi 6508 nnaordr 6510 fvixp 6702 cbvixp 6714 mptelixpg 6733 exmidaclem 7206 cc1 7263 cc2lem 7264 cc3 7266 ltapig 7336 ltmpig 7337 fzsubel 10057 elfzp1b 10094 ennnfonelemg 12398 ennnfonelemp1 12401 ennnfonelemnn0 12417 ctiunctlemu1st 12429 ctiunctlemu2nd 12430 ctiunctlemudc 12432 ctiunctlemfo 12434 ismgm 12730 mgm1 12743 ismndd 12792 eqgfval 13034 ringcl 13149 unitinvcl 13245 aprval 13293 aprap 13297 istps 13423 tpspropd 13427 eltpsg 13431 isms 13846 mspropd 13871 cnlimci 14035 |
Copyright terms: Public domain | W3C validator |