![]() |
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 2243 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 146 |
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: eqeltrri 2251 3eltr4i 2259 intab 3873 inex2 4137 vpwex 4178 ord3ex 4189 uniopel 4255 onsucelsucexmid 4528 nnpredcl 4621 elvvuni 4689 isarep2 5302 acexmidlemcase 5867 abrexex2 6122 oprabex 6126 oprabrexex2 6128 mpoexw 6211 rdg0 6385 frecex 6392 1on 6421 2on 6423 3on 6425 4on 6426 1onn 6518 2onn 6519 3onn 6520 4onn 6521 mapsnf1o2 6693 exmidpw 6905 unfiexmid 6914 xpfi 6926 ssfirab 6930 fnfi 6933 iunfidisj 6942 fidcenumlemr 6951 sbthlemi10 6962 ctmlemr 7104 nninfex 7117 exmidonfinlem 7189 acfun 7203 exmidaclem 7204 pw1ne1 7225 ccfunen 7260 nqex 7359 nq0ex 7436 1pr 7550 ltexprlempr 7604 recexprlempr 7628 cauappcvgprlemcl 7649 caucvgprlemcl 7672 caucvgprprlemcl 7700 addvalex 7840 peano1nnnn 7848 peano2nnnn 7849 axcnex 7855 ax1cn 7857 ax1re 7858 pnfxr 8006 mnfxr 8010 inelr 8537 cju 8914 2re 8985 3re 8989 4re 8992 5re 8994 6re 8996 7re 8998 8re 9000 9re 9002 2nn 9076 3nn 9077 4nn 9078 5nn 9079 6nn 9080 7nn 9081 8nn 9082 9nn 9083 nn0ex 9178 nneoor 9351 zeo 9354 deccl 9394 decnncl 9399 numnncl2 9402 decnncl2 9403 numsucc 9419 numma2c 9425 numadd 9426 numaddc 9427 nummul1c 9428 nummul2c 9429 xnegcl 9828 xrex 9852 ioof 9967 uzennn 10431 seqex 10442 m1expcl2 10537 faccl 10708 facwordi 10713 faclbnd2 10715 bccl 10740 crre 10859 remim 10862 absval 11003 climle 11335 climcvg1nlem 11350 iserabs 11476 geo2lim 11517 prodfclim1 11545 fprodle 11641 ere 11671 ege2le3 11672 eftlub 11691 efsep 11692 tan0 11732 ef01bndlem 11757 nn0o 11904 pczpre 12289 pockthi 12348 igz 12364 ennnfonelemj0 12394 ennnfonelem0 12398 ndxarg 12477 ndxslid 12479 strndxid 12482 basendxnn 12510 strle1g 12557 plusgndxnn 12562 2strbasg 12570 2stropg 12571 tsetndxnn 12636 plendxnn 12650 dsndxnn 12661 unifndxnn 12671 setsmsbasg 13850 cnbl0 13905 cnopncntop 13908 remet 13911 divcnap 13926 climcncf 13942 expcncf 13963 cnrehmeocntop 13964 sincn 14061 coscn 14062 2logb9irrALT 14263 2irrexpq 14265 2irrexpqap 14267 lgslem4 14275 lgsdir2lem2 14301 bdinex2 14512 bj-inex 14519 012of 14605 2o01f 14606 peano3nninf 14616 cvgcmp2nlemabs 14640 trilpolemisumle 14646 |
Copyright terms: Public domain | W3C validator |