Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eleqtri | Structured version Visualization 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 2693 | . 2 |
4 | 1, 3 | mpbi 220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 wcel 1990 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-clel 2618 |
This theorem is referenced by: eleqtrri 2700 3eltr3i 2713 prid2 4298 2eluzge0 11733 fz0to4untppr 12442 seqp1i 12817 faclbnd4lem1 13080 cats1fv 13604 bpoly2 14788 bpoly3 14789 bpoly4 14790 ef0lem 14809 phi1 15478 gsumws1 17376 lt6abl 18296 uvcvvcl 20126 smadiadetlem4 20475 indiscld 20895 cnrehmeo 22752 ovolicc1 23284 dvcjbr 23712 vieta1lem2 24066 dvloglem 24394 logdmopn 24395 efopnlem2 24403 cxpcn 24486 loglesqrt 24499 log2ublem2 24674 efrlim 24696 tgcgr4 25426 axlowdimlem16 25837 axlowdimlem17 25838 nlelchi 28920 hmopidmchi 29010 raddcn 29975 xrge0tmd 29992 indf 30077 ballotlem1ri 30596 chtvalz 30707 circlemethhgt 30721 dvtanlem 33459 ftc1cnnc 33484 dvasin 33496 dvacos 33497 dvreasin 33498 dvreacos 33499 areacirclem2 33501 areacirclem4 33503 cncfres 33564 jm2.23 37563 fvnonrel 37903 frege54cor1c 38209 fourierdlem28 40352 fourierdlem57 40380 fourierdlem59 40382 fourierdlem62 40385 fourierdlem68 40391 fouriersw 40448 etransclem23 40474 etransclem35 40486 etransclem38 40489 etransclem39 40490 etransclem44 40495 etransclem45 40496 etransclem47 40498 rrxtopn0 40513 hoidmvlelem2 40810 vonicclem2 40898 fmtno4prmfac 41484 |
Copyright terms: Public domain | W3C validator |