Theorem eqeltrrd 2309

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrrd	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2308	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ 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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

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

This theorem is referenced by:  3eltr3d  2314  exmid01  4294  pwntru  4295  xpexr2m  5185  funimaexg  5421  fndmexd  5534  fvmptdv2  5745  ffvresb  5818  iotaexel  5986  2ndrn  6355  1st2ndbr  6356  elopabi  6369  cnvf1olem  6398  dftpos4  6472  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  nnmordi  6727  th3qlem1  6849  infiexmid  7109  onunsnss  7152  ssfirab  7172  ssfidc  7173  fnfi  7178  fidcenumlemr  7197  elfi2  7214  ordiso2  7277  djulclb  7297  ctmlemr  7350  ctssdccl  7353  ctssdc  7355  exmidfodomrlemreseldju  7454  exmidfodomrlemr  7456  pw1m  7485  exmidapne  7522  archnqq  7680  prarloclemarch2  7682  enq0tr  7697  nqnq0  7704  addcmpblnq0  7706  mulcmpblnq0  7707  mulcanenq0ec  7708  addclnq0  7714  mulclnq0  7715  nqpnq0nq  7716  nq0m0r  7719  distrnq0  7722  addassnq0lemcl  7724  prarloclemlt  7756  prarloclem5  7763  distrlem4prl  7847  distrlem4pru  7848  ltexprlemm  7863  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  cauappcvgprlemladdru  7919  prsrlem1  8005  mulgt0sr  8041  axpre-suploclemres  8164  cnegexlem2  8398  subf  8424  resubcl  8486  negcon1ad  8528  subeq0bd  8601  rimul  8808  rereim  8809  aprcl  8869  nn0nnaddcl  9476  elnn0nn  9487  zaddcllemneg  9561  zsubcl  9563  zrevaddcl  9573  elz2  9594  zdiv  9611  peano5uzti  9631  peano2uzr  9862  uzaddcl  9863  divfnzn  9898  qsubcl  9915  qrevaddcl  9921  fseq1p1m1  10372  suprzubdc  10540  modqmuladdim  10673  frec2uzrand  10711  frecuzrdglem  10717  frecuzrdg0  10719  frecuzrdgdomlem  10723  frecuzrdg0t  10728  frecuzrdgsuctlem  10729  seq3val  10766  seq3feq  10786  iseqf1olemnab  10807  seqf1oglem2  10826  seqfeq3  10835  seqfeq4g  10837  expaddzaplem  10888  expaddzap  10889  expmulzap  10891  zesq  10964  bcm1k  11066  bccl  11073  permnn  11077  seq3coll  11150  ccatrn  11233  shftuz  11438  ref  11476  imf  11477  crre  11478  rereb  11484  resqrexlemnm  11639  absf  11731  summodclem2a  12003  summodc  12005  fsumgcl  12008  fsum3  12009  fsumf1o  12012  fsumcnv  12059  mptfzshft  12064  isumlessdc  12118  geolim2  12134  prodmodclem3  12197  fprodseq  12205  fprodf1o  12210  dvdsaddre2b  12463  3dvds  12486  oexpneg  12499  nn0ob  12530  divalglemqt  12541  gcdf  12604  lcmgcdlem  12710  sqnprm  12769  sqrt2irrlem  12794  2sqpwodd  12809  fnum  12823  fden  12824  phimullem  12858  pc2dvds  12964  gzsubcl  13014  4sqlem5  13016  4sqlem9  13020  4sqlem10  13021  mul4sqlem  13027  mul4sq  13028  4sqlem11  13035  4sqlem13m  13037  4sqlem16  13040  4sqlem17  13041  4sqlem18  13042  ctiunctlemfo  13121  ptex  13408  prdsval  13417  prdsbas  13420  prdsbascl  13433  mgmsscl  13505  subsubm  13627  mhmima  13635  imasgrp2  13758  mhmmnd  13764  mulgdir  13802  subgmulg  13836  issubg2m  13837  issubgrpd2  13838  grpissubg  13842  subsubg  13845  isnsg3  13855  ssnmz  13859  eqger  13872  eqgen  13875  ecqusaddcl  13887  ghmrn  13905  ghmnsgima  13916  conjsubg  13925  conjnmz  13927  ring1  14134  dvdsrvald  14169  dvdsrd  14170  dvdsrex  14174  0unit  14205  invrpropdg  14225  lringuplu  14272  subrngin  14289  subsubrng  14290  subrgcrng  14301  subrgin  14320  subsubrg  14321  islmodd  14369  lssvacl  14441  lssvancl1  14443  lss0cl  14445  lssvscl  14451  lssvnegcl  14452  lssincl  14461  issubrgd  14528  lidlrsppropdg  14571  2idlcpblrng  14599  zsssubrg  14661  unopn  14796  tsettps  14829  tgss2  14870  difopn  14899  resttop  14961  resttopon  14962  restco  14965  tgcn  14999  tgcnp  15000  cnptopco  15013  upxp  15063  txcn  15066  txdis  15068  cnmpt11  15074  cnmpt11f  15075  cnmpt1t  15076  cnmpt12  15078  cnmpt21  15082  cnmpt21f  15083  cnmpt2t  15084  cnmpt22  15085  cnmpt22f  15086  cnmpt1res  15087  xmeter  15227  mscl  15256  xmscl  15257  bdxmet  15292  cncfmpt1f  15389  cdivcncfap  15395  negfcncf  15397  ivthreinc  15436  cnmptlimc  15465  dvcnp2cntop  15490  elplyd  15532  plypow  15535  plyconst  15536  plyaddlem1  15538  plysub  15544  dvply2g  15557  sincn  15560  coscn  15561  relogcl  15653  mpodvdsmulf1o  15784  fsumdvdsmul  15785  mersenne  15791  perfect  15795  lgsne0  15837  lgseisenlem4  15872  lgsquadlem1  15876  usgr1vr  16169  p1evtxdeqfilem  16232  isclwwlkn  16334  clwwlknon  16350  pwtrufal  16699  repiecele0  16738  qdiff  16761  gfsumcl  16796