Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eleqtrrid | Structured version Visualization version GIF version |
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eleqtrrid.1 | ⊢ 𝐴 ∈ 𝐵 |
eleqtrrid.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
Ref | Expression |
---|---|
eleqtrrid | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrrid.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | eleqtrrid.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
3 | 2 | eqcomd 2827 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | eleqtrid 2919 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 df-clel 2893 |
This theorem is referenced by: rabsnt 4667 onnev 6311 opabiota 6746 canth 7111 onnseq 7981 tfrlem16 8029 oen0 8212 nnawordex 8263 inf0 9084 cantnflt 9135 cnfcom2 9165 cnfcom3lem 9166 cnfcom3 9167 r1ordg 9207 r1val1 9215 rankr1id 9291 acacni 9566 dfacacn 9567 dfac13 9568 ttukeylem5 9935 ttukeylem6 9936 gch2 10097 gch3 10098 gchac 10103 gchina 10121 swrds1 14028 wrdl3s3 14326 sadcp1 15804 lcmfunsnlem2 15984 fnpr2ob 16831 idfucl 17151 gsumval2 17896 gsumz 18000 frmdmnd 18024 frmd0 18025 efginvrel2 18853 efgcpbl2 18883 pgpfaclem1 19203 lbsexg 19936 zringndrg 20637 frlmlbs 20941 mat0dimscm 21078 mat0scmat 21147 m2detleiblem5 21234 m2detleiblem6 21235 m2detleiblem3 21238 m2detleiblem4 21239 d0mat2pmat 21346 chpmat0d 21442 dfac14 22226 acufl 22525 cnextfvval 22673 cnextcn 22675 minveclem3b 24031 minveclem4a 24033 ovollb2 24090 ovolunlem1a 24097 ovolunlem1 24098 ovoliunlem1 24103 ovoliun2 24107 ioombl1lem4 24162 uniioombllem1 24182 uniioombllem2 24184 uniioombllem6 24189 itg2monolem1 24351 itg2mono 24354 itg2cnlem1 24362 xrlimcnp 25546 efrlim 25547 eengbas 26767 ebtwntg 26768 ecgrtg 26769 elntg 26770 wlkl1loop 27419 elwwlks2ons3im 27733 upgr3v3e3cycl 27959 upgr4cycl4dv4e 27964 2clwwlk2clwwlk 28129 ex-br 28210 trsp2cyc 30765 cyc3evpm 30792 lvecdim0 31005 extdg1id 31053 rge0scvg 31192 repr0 31882 hgt750lemg 31925 mrsub0 32763 elmrsubrn 32767 topjoin 33713 finorwe 34666 pclfinN 37051 aomclem1 39703 dfac21 39715 clsk1indlem1 40444 mnurndlem1 40666 fourierdlem102 42542 fourierdlem114 42554 lincval0 44519 lcoel0 44532 |
Copyright terms: Public domain | W3C validator |