Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleqtrrd | Unicode version |
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
eleqtrrd.1 | |
eleqtrrd.2 |
Ref | Expression |
---|---|
eleqtrrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrrd.1 | . 2 | |
2 | eleqtrrd.2 | . . 3 | |
3 | 2 | eqcomd 2145 | . 2 |
4 | 1, 3 | eleqtrd 2218 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wcel 1480 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 |
This theorem is referenced by: 3eltr4d 2223 exmidsssnc 4126 tfrexlem 6231 nnsucuniel 6391 erref 6449 en1uniel 6698 fin0 6779 fin0or 6780 prarloclemarch2 7227 fzopth 9841 fzoss2 9949 fzosubel3 9973 elfzomin 9983 elfzonlteqm1 9987 fzoend 9999 fzofzp1 10004 fzofzp1b 10005 peano2fzor 10009 zmodfzo 10120 frecuzrdg0 10186 frecuzrdgsuc 10187 frecuzrdgdomlem 10190 frecuzrdg0t 10195 frecuzrdgsuctlem 10196 seq3f1olemqsum 10273 bcn2 10510 summodclem2a 11150 fisumss 11161 fsumm1 11185 fisumcom2 11207 prodmodclem2a 11345 ennnfonelemex 11927 ctinfomlemom 11940 lmtopcnp 12419 txopn 12434 blpnfctr 12608 metcnpi 12684 metcnpi2 12685 cncfmpt2fcntop 12754 limcimolemlt 12802 cnplimclemr 12807 limccnp2lem 12814 limccnp2cntop 12815 dvidlemap 12829 dvcnp2cntop 12832 dvcn 12833 dvaddxxbr 12834 dvmulxxbr 12835 dvef 12856 |
Copyright terms: Public domain | W3C validator |