| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eleqtri | Structured version Visualization version GIF version | ||
| Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.) |
| Ref | Expression |
|---|---|
| eleqtri.1 | ⊢ 𝐴 ∈ 𝐵 |
| eleqtri.2 | ⊢ 𝐵 = 𝐶 |
| Ref | Expression |
|---|---|
| eleqtri | ⊢ 𝐴 ∈ 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleqtri.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
| 2 | eleqtri.2 | . . 3 ⊢ 𝐵 = 𝐶 | |
| 3 | 2 | eleq2i 2833 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶) |
| 4 | 1, 3 | mpbi 230 | 1 ⊢ 𝐴 ∈ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: eleqtrri 2840 3eltr3i 2853 prid2 4763 2eluzge0 12935 faclbnd4lem1 14332 cats1fv 14898 bpoly2 16093 bpoly3 16094 bpoly4 16095 ef0lem 16114 phi1 16810 gsumws1 18851 lt6abl 19913 uvcvvcl 21807 mhpvarcl 22152 smadiadetlem4 22675 indiscld 23099 cnrehmeo 24984 cnrehmeoOLD 24985 ovolicc1 25551 dvcjbr 25987 vieta1lem2 26353 dvloglem 26690 logdmopn 26691 efopnlem2 26699 cxpcn 26787 cxpcnOLD 26788 loglesqrt 26804 log2ublem2 26990 efrlim 27012 efrlimOLD 27013 precsexlem11 28241 tgcgr4 28539 axlowdimlem16 28972 axlowdimlem17 28973 nlelchi 32080 hmopidmchi 32170 indf 32840 evl1deg2 33602 evl1deg3 33603 raddcn 33928 xrge0tmd 33944 ballotlem1ri 34537 chtvalz 34644 circlemethhgt 34658 dvtanlem 37676 ftc1cnnc 37699 dvasin 37711 dvacos 37712 dvreasin 37713 dvreacos 37714 areacirclem2 37716 areacirclem4 37718 cncfres 37772 resuppsinopn 42393 jm2.23 43008 0finon 43461 1finon 43462 2finon 43463 3finon 43464 4finon 43465 fvnonrel 43610 frege54cor1c 43928 fourierdlem28 46150 fourierdlem57 46178 fourierdlem59 46180 fourierdlem62 46183 fourierdlem68 46189 fouriersw 46246 etransclem23 46272 etransclem35 46284 etransclem38 46287 etransclem39 46288 etransclem44 46293 etransclem45 46294 etransclem47 46296 rrxtopn0 46308 hoidmvlelem2 46611 vonicclem2 46699 fmtno4prmfac 47559 gpg5grlic 48047 |
| Copyright terms: Public domain | W3C validator |