Theorem eleqtrd 2317

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrrd  2318  3eltr3d  2321  eleqtrid  2327  eleqtrdi  2331  sn0disj  4127  opth1  4378  0nelop  4390  tfisi  4736  nnpredlt  4773  iotam  5372  ercl  6823  erth  6858  ecelqsdm  6884  phpm  7173  exmidpweq  7222  pw1if  7590  cc2lem  7638  cc3  7640  suplocexprlemmu  8091  suplocexprlemloc  8094  lincmb01cmp  10421  fzopth  10483  fzoaddel2  10624  fzosubel2  10629  fzocatel  10633  zpnn0elfzo1  10642  fzoend  10656  peano2fzor  10666  infssfzcldc  10685  infssfzledc  10686  monoord2  10943  ser3mono  10944  bcpasc  11225  zfz1isolemiso  11312  swrdclg  11443  fisum0diag2  12238  isumsplit  12282  prodmodclem3  12366  prodmodclem2a  12367  nnmindc  12835  nnminle  12836  bassetsnn  13466  basmexd  13470  basm  13471  slotm  13472  mgm1  13748  grpidd  13761  gzsumress  13770  sgrppropd  13786  ismndd  13808  mndpropd  13811  issubmnd  13813  imasmnd  13818  grpidd2  13904  imasgrp  13972  submmulg  14027  subginvcl  14044  subgcl  14045  subgsub  14047  subgmulg  14049  1nsgtrivd  14080  quseccl0g  14092  kerf1ghm  14135  prdsbasfn  14287  prdsbasprj  14288  pwsplusgval  14314  pwsmulrval  14315  pwsinvg  14321  rngass  14344  rngcl  14349  rngpropd  14360  imasrng  14361  srgcl  14380  srgass  14381  srgpcomp  14400  srgpcompp  14401  srgpcomppsc  14402  crngcom  14424  ringass  14426  ringidmlem  14433  ringidss  14440  ringpropd  14449  imasring  14477  qusring2  14479  mulgass3  14499  dvdsrd  14509  1unit  14522  unitmulcl  14528  dvrvald  14549  rdivmuldivd  14559  elrhmunit  14592  rhmunitinv  14593  lringuplu  14611  subrngmcl  14625  subrg1  14647  subrgmcl  14649  subrgdv  14654  subrgunit  14655  resrhm  14664  aprval  14699  aprirr  14703  aprsym  14704  aprcotr  14705  opprdrng  14728  lmodprop2d  14793  lidlss  14921  lidl0cl  14928  lidlacl  14929  lidlnegcl  14930  rnglidlmsgrp  14942  2idllidld  14951  2idlridld  14952  2idlcpblrng  14968  qus1  14971  quscrng  14978  rspsn  14979  znf1o  15094  assapropd  15122  psrbagfi  15166  psrbagdceq  15167  psrbaglefifi  15175  psrelbas  15188  psrmulvalfi  15197  mplsubgfileminv  15233  iscnp4  15461  cnrest2r  15480  txbasval  15510  txlm  15522  xmetunirn  15601  xblss2ps  15647  blbas  15676  mopntopon  15686  isxms2  15695  metcnpi  15758  metcnpi2  15759  tgioo  15797  cncfmpt2fcntop  15842  limccl  15902  limcimolemlt  15907  limccnp2cntop  15920  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  ppinprm  16277  chtnprm  16279  lgseisenlem4  16414  usgr1vr  16711  clwwlkccatlem  16863