![]() |
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 2829 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶) |
4 | 1, 3 | mpbi 229 | 1 ⊢ 𝐴 ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-clel 2814 |
This theorem is referenced by: eleqtrri 2837 3eltr3i 2850 prid2 4724 2eluzge0 12818 fz0to4untppr 13544 faclbnd4lem1 14193 cats1fv 14748 bpoly2 15940 bpoly3 15941 bpoly4 15942 ef0lem 15961 phi1 16645 gsumws1 18648 lt6abl 19672 uvcvvcl 21193 mhpvarcl 21538 smadiadetlem4 22018 indiscld 22442 cnrehmeo 24316 ovolicc1 24880 dvcjbr 25313 vieta1lem2 25671 dvloglem 26003 logdmopn 26004 efopnlem2 26012 cxpcn 26098 loglesqrt 26111 log2ublem2 26297 efrlim 26319 tgcgr4 27473 axlowdimlem16 27906 axlowdimlem17 27907 nlelchi 31003 hmopidmchi 31093 raddcn 32510 xrge0tmd 32526 indf 32614 ballotlem1ri 33134 chtvalz 33242 circlemethhgt 33256 dvtanlem 36127 ftc1cnnc 36150 dvasin 36162 dvacos 36163 dvreasin 36164 dvreacos 36165 areacirclem2 36167 areacirclem4 36169 cncfres 36224 jm2.23 41306 0finon 41710 1finon 41711 2finon 41712 3finon 41713 4finon 41714 fvnonrel 41859 frege54cor1c 42177 fourierdlem28 44366 fourierdlem57 44394 fourierdlem59 44396 fourierdlem62 44399 fourierdlem68 44405 fouriersw 44462 etransclem23 44488 etransclem35 44500 etransclem38 44503 etransclem39 44504 etransclem44 44509 etransclem45 44510 etransclem47 44512 rrxtopn0 44524 hoidmvlelem2 44827 vonicclem2 44915 fmtno4prmfac 45754 |
Copyright terms: Public domain | W3C validator |