Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeltri | Unicode version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeltr.1 | |
eqeltr.2 |
Ref | Expression |
---|---|
eqeltri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltr.2 | . 2 | |
2 | eqeltr.1 | . . 3 | |
3 | 2 | eleq1i 2183 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 wcel 1465 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 df-clel 2113 |
This theorem is referenced by: eqeltrri 2191 3eltr4i 2199 intab 3770 inex2 4033 vpwex 4073 ord3ex 4084 uniopel 4148 onsucelsucexmid 4415 nnpredcl 4506 elvvuni 4573 isarep2 5180 acexmidlemcase 5737 abrexex2 5990 oprabex 5994 oprabrexex2 5996 rdg0 6252 frecex 6259 1on 6288 2on 6290 3on 6292 4on 6293 1onn 6384 2onn 6385 3onn 6386 4onn 6387 mapsnf1o2 6558 exmidpw 6770 unfiexmid 6774 xpfi 6786 ssfirab 6790 fnfi 6793 iunfidisj 6802 fidcenumlemr 6811 sbthlemi10 6822 ctmlemr 6961 exmidonfinlem 7017 acfun 7031 exmidaclem 7032 ccfunen 7047 nqex 7139 nq0ex 7216 1pr 7330 ltexprlempr 7384 recexprlempr 7408 cauappcvgprlemcl 7429 caucvgprlemcl 7452 caucvgprprlemcl 7480 addvalex 7620 peano1nnnn 7628 peano2nnnn 7629 axcnex 7635 ax1cn 7637 ax1re 7638 pnfxr 7786 mnfxr 7790 inelr 8314 cju 8687 2re 8758 3re 8762 4re 8765 5re 8767 6re 8769 7re 8771 8re 8773 9re 8775 2nn 8849 3nn 8850 4nn 8851 5nn 8852 6nn 8853 7nn 8854 8nn 8855 9nn 8856 nn0ex 8951 nneoor 9121 zeo 9124 deccl 9164 decnncl 9169 numnncl2 9172 decnncl2 9173 numsucc 9189 numma2c 9195 numadd 9196 numaddc 9197 nummul1c 9198 nummul2c 9199 xnegcl 9583 xrex 9607 ioof 9722 uzennn 10177 seqex 10188 m1expcl2 10283 faccl 10449 facwordi 10454 faclbnd2 10456 bccl 10481 crre 10597 remim 10600 absval 10741 climle 11071 climcvg1nlem 11086 iserabs 11212 geo2lim 11253 ere 11303 ege2le3 11304 eftlub 11323 efsep 11324 tan0 11365 ef01bndlem 11390 nn0o 11531 ennnfonelemj0 11841 ennnfonelem0 11845 ndxarg 11909 ndxslid 11911 strndxid 11914 basendxnn 11941 strle1g 11976 2strbasg 11987 2stropg 11988 setsmsbasg 12575 cnbl0 12630 cnopncntop 12633 remet 12636 divcnap 12651 climcncf 12667 expcncf 12688 cnrehmeocntop 12689 sincn 12785 coscn 12786 bdinex2 13025 bj-inex 13032 peano3nninf 13128 nninfex 13132 isomninnlem 13152 cvgcmp2nlemabs 13154 trilpolemisumle 13158 |
Copyright terms: Public domain | W3C validator |