Theorem eleqtrd 2310

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2301	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleqtrrd  2311  3eltr3d  2314  eleqtrid  2320  eleqtrdi  2324  opth1  4328  0nelop  4340  tfisi  4685  nnpredlt  4722  iotam  5318  ercl  6713  erth  6748  ecelqsdm  6774  phpm  7052  exmidpweq  7101  pw1if  7443  cc2lem  7485  cc3  7487  suplocexprlemmu  7938  suplocexprlemloc  7941  lincmb01cmp  10238  fzopth  10296  fzoaddel2  10436  fzosubel2  10441  fzocatel  10445  zpnn0elfzo1  10454  fzoend  10468  peano2fzor  10478  monoord2  10749  ser3mono  10750  bcpasc  11029  zfz1isolemiso  11104  swrdclg  11232  fisum0diag2  12010  isumsplit  12054  prodmodclem3  12138  prodmodclem2a  12139  nnmindc  12607  nnminle  12608  bassetsnn  13141  basmexd  13145  basm  13146  prdsbasfn  13366  prdsbasprj  13367  pwsplusgval  13380  pwsmulrval  13381  mgm1  13455  grpidd  13468  gsumress  13480  sgrppropd  13498  ismndd  13522  mndpropd  13525  issubmnd  13527  imasmnd  13538  grpidd2  13626  pwsinvg  13697  imasgrp  13700  submmulg  13755  subginvcl  13772  subgcl  13773  subgsub  13775  subgmulg  13777  1nsgtrivd  13808  quseccl0g  13820  kerf1ghm  13863  rngass  13955  rngcl  13960  rngpropd  13971  imasrng  13972  srgcl  13986  srgass  13987  srg1zr  14003  srgpcomp  14006  srgpcompp  14007  srgpcomppsc  14008  crngcom  14030  ringass  14032  ringidmlem  14038  ringidss  14045  ringpropd  14054  imasring  14080  qusring2  14082  mulgass3  14101  dvdsrd  14111  1unit  14124  unitmulcl  14130  dvrvald  14151  rdivmuldivd  14161  elrhmunit  14194  rhmunitinv  14195  lringuplu  14213  subrngmcl  14226  subrg1  14248  subrgmcl  14250  subrgdv  14255  subrgunit  14256  resrhm  14265  aprval  14299  aprirr  14300  aprsym  14301  aprcotr  14302  lmodprop2d  14365  lidlss  14493  lidl0cl  14500  lidlacl  14501  lidlnegcl  14502  rnglidlmsgrp  14514  2idllidld  14523  2idlridld  14524  2idlcpblrng  14540  qus1  14543  quscrng  14550  rspsn  14551  znf1o  14668  psrbagfi  14690  psrelbas  14692  iscnp4  14945  cnrest2r  14964  txbasval  14994  txlm  15006  xmetunirn  15085  xblss2ps  15131  blbas  15160  mopntopon  15170  isxms2  15179  metcnpi  15242  metcnpi2  15243  tgioo  15281  cncfmpt2fcntop  15326  limccl  15386  limcimolemlt  15391  limccnp2cntop  15404  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  dvrecap  15440  plyaddlem1  15474  plymullem1  15475  plycoeid3  15484  lgseisenlem4  15805  usgr1vr  16102  clwwlkccatlem  16254