![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > eleqtri | Structured version Unicode version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
Ref | Expression |
---|---|
eleqtr.1 |
![]() ![]() ![]() ![]() |
eleqtr.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eleqtri |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtr.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eleqtr.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eleq2i 2530 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbi 208 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-ext 2431 |
This theorem depends on definitions: df-bi 185 df-an 371 df-ex 1588 df-cleq 2444 df-clel 2447 |
This theorem is referenced by: eleqtrri 2539 3eltr3i 2552 prid2 4087 seqp1i 11934 faclbnd4lem1 12181 bcn1 12201 bcpasc 12209 cats1fv 12599 ef0lem 13477 phi1 13961 dfphi2 13962 gsumws1 15631 efgsp1 16350 efgsres 16351 efgredlemd 16357 efgredlem 16360 lt6abl 16487 uvcvvcl 18332 smadiadetlem4 18602 indiscld 18822 cnrehmeo 20652 ovolicc1 21126 iblcnlem1 21393 dvcjbr 21551 c1lip2 21598 dvply1 21878 vieta1lem2 21905 dvtaylp 21963 taylthlem2 21967 dvloglem 22221 logdmopn 22222 efopnlem2 22230 logtayl 22233 cxpcn 22311 loglesqr 22324 leibpilem2 22464 log2ublem2 22470 efrlim 22491 basellem5 22550 ppiltx 22643 prmorcht 22644 chtlepsi 22673 chpub 22687 chebbnd1lem1 22846 chtppilimlem1 22850 axlowdimlem16 23350 axlowdimlem17 23351 axlowdim 23354 usgraexvlem 23460 konigsberg 23755 nlelchi 25612 hmopidmchi 25702 raddcn 26499 xrge0tmd 26516 indf 26612 ballotlemfrci 27049 ballotlemfrceq 27050 ballotlem1ri 27056 signsvfn 27122 bpoly2 28339 bpoly3 28340 bpoly4 28341 dvtanlem 28584 ftc1cnnc 28609 dvasin 28623 dvacos 28624 dvreasin 28625 dvreacos 28626 areacirclem2 28628 areacirclem4 28630 cncfres 28807 jm2.23 29488 |
Copyright terms: Public domain | W3C validator |