Theorem eleqtrd 2311

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 2302	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eleqtrrd  2312  3eltr3d  2315  eleqtrid  2321  eleqtrdi  2325  opth1  4352  0nelop  4364  tfisi  4709  nnpredlt  4746  iotam  5344  ercl  6778  erth  6813  ecelqsdm  6839  phpm  7120  exmidpweq  7169  pw1if  7535  cc2lem  7580  cc3  7582  suplocexprlemmu  8033  suplocexprlemloc  8036  lincmb01cmp  10336  fzopth  10395  fzoaddel2  10535  fzosubel2  10540  fzocatel  10544  zpnn0elfzo1  10553  fzoend  10567  peano2fzor  10577  monoord2  10848  ser3mono  10849  bcpasc  11128  zfz1isolemiso  11211  swrdclg  11342  fisum0diag2  12133  isumsplit  12177  prodmodclem3  12261  prodmodclem2a  12262  nnmindc  12730  nnminle  12731  bassetsnn  13269  basmexd  13273  basm  13274  prdsbasfn  13494  prdsbasprj  13495  pwsplusgval  13508  pwsmulrval  13509  mgm1  13583  grpidd  13596  gsumress  13608  sgrppropd  13626  ismndd  13650  mndpropd  13653  issubmnd  13655  imasmnd  13666  grpidd2  13754  pwsinvg  13825  imasgrp  13828  submmulg  13883  subginvcl  13900  subgcl  13901  subgsub  13903  subgmulg  13905  1nsgtrivd  13936  quseccl0g  13948  kerf1ghm  13991  rngass  14083  rngcl  14088  rngpropd  14099  imasrng  14100  srgcl  14114  srgass  14115  srg1zr  14131  srgpcomp  14134  srgpcompp  14135  srgpcomppsc  14136  crngcom  14158  ringass  14160  ringidmlem  14166  ringidss  14173  ringpropd  14182  imasring  14208  qusring2  14210  mulgass3  14229  dvdsrd  14239  1unit  14252  unitmulcl  14258  dvrvald  14279  rdivmuldivd  14289  elrhmunit  14322  rhmunitinv  14323  lringuplu  14341  subrngmcl  14354  subrg1  14376  subrgmcl  14378  subrgdv  14383  subrgunit  14384  resrhm  14393  aprval  14428  aprirr  14429  aprsym  14430  aprcotr  14431  lmodprop2d  14496  lidlss  14624  lidl0cl  14631  lidlacl  14632  lidlnegcl  14633  rnglidlmsgrp  14645  2idllidld  14654  2idlridld  14655  2idlcpblrng  14671  qus1  14674  quscrng  14681  rspsn  14682  znf1o  14799  psrbagfi  14823  psrelbas  14830  iscnp4  15083  cnrest2r  15102  txbasval  15132  txlm  15144  xmetunirn  15223  xblss2ps  15269  blbas  15298  mopntopon  15308  isxms2  15317  metcnpi  15380  metcnpi2  15381  tgioo  15419  cncfmpt2fcntop  15464  limccl  15524  limcimolemlt  15529  limccnp2cntop  15542  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvrecap  15578  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  lgseisenlem4  15946  usgr1vr  16243  clwwlkccatlem  16395