Theorem eqeltrrd 2307

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 2235	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2306	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  3eltr3d  2312  exmid01  4282  pwntru  4283  xpexr2m  5170  funimaexg  5405  fvmptdv2  5724  ffvresb  5798  iotaexel  5959  2ndrn  6329  1st2ndbr  6330  elopabi  6341  cnvf1olem  6370  dftpos4  6409  tfrlemibxssdm  6473  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  nnmordi  6662  th3qlem1  6784  infiexmid  7039  onunsnss  7079  ssfirab  7098  ssfidc  7099  fnfi  7103  fidcenumlemr  7122  elfi2  7139  ordiso2  7202  djulclb  7222  ctmlemr  7275  ctssdccl  7278  ctssdc  7280  exmidfodomrlemreseldju  7378  exmidfodomrlemr  7380  pw1m  7409  exmidapne  7446  archnqq  7604  prarloclemarch2  7606  enq0tr  7621  nqnq0  7628  addcmpblnq0  7630  mulcmpblnq0  7631  mulcanenq0ec  7632  addclnq0  7638  mulclnq0  7639  nqpnq0nq  7640  nq0m0r  7643  distrnq0  7646  addassnq0lemcl  7648  prarloclemlt  7680  prarloclem5  7687  distrlem4prl  7771  distrlem4pru  7772  ltexprlemm  7787  ltexprlemrl  7797  ltexprlemru  7799  addcanprleml  7801  cauappcvgprlemladdru  7843  prsrlem1  7929  mulgt0sr  7965  axpre-suploclemres  8088  cnegexlem2  8322  subf  8348  resubcl  8410  negcon1ad  8452  subeq0bd  8525  rimul  8732  rereim  8733  aprcl  8793  nn0nnaddcl  9400  elnn0nn  9411  zaddcllemneg  9485  zsubcl  9487  zrevaddcl  9497  elz2  9518  zdiv  9535  peano5uzti  9555  peano2uzr  9780  uzaddcl  9781  divfnzn  9816  qsubcl  9833  qrevaddcl  9839  fseq1p1m1  10290  suprzubdc  10456  modqmuladdim  10589  frec2uzrand  10627  frecuzrdglem  10633  frecuzrdg0  10635  frecuzrdgdomlem  10639  frecuzrdg0t  10644  frecuzrdgsuctlem  10645  seq3val  10682  seq3feq  10702  iseqf1olemnab  10723  seqf1oglem2  10742  seqfeq3  10751  seqfeq4g  10753  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  zesq  10880  bcm1k  10982  bccl  10989  permnn  10993  seq3coll  11064  ccatrn  11144  shftuz  11328  ref  11366  imf  11367  crre  11368  rereb  11374  resqrexlemnm  11529  absf  11621  summodclem2a  11892  summodc  11894  fsumgcl  11897  fsum3  11898  fsumf1o  11901  fsumcnv  11948  mptfzshft  11953  isumlessdc  12007  geolim2  12023  prodmodclem3  12086  fprodseq  12094  fprodf1o  12099  dvdsaddre2b  12352  3dvds  12375  oexpneg  12388  nn0ob  12419  divalglemqt  12430  gcdf  12493  lcmgcdlem  12599  sqnprm  12658  sqrt2irrlem  12683  2sqpwodd  12698  fnum  12712  fden  12713  phimullem  12747  pc2dvds  12853  gzsubcl  12903  4sqlem5  12905  4sqlem9  12909  4sqlem10  12910  mul4sqlem  12916  mul4sq  12917  4sqlem11  12924  4sqlem13m  12926  4sqlem16  12929  4sqlem17  12930  4sqlem18  12931  ctiunctlemfo  13010  ptex  13297  prdsval  13306  prdsbas  13309  prdsbascl  13322  mgmsscl  13394  subsubm  13516  mhmima  13524  imasgrp2  13647  mhmmnd  13653  mulgdir  13691  subgmulg  13725  issubg2m  13726  issubgrpd2  13727  grpissubg  13731  subsubg  13734  isnsg3  13744  ssnmz  13748  eqger  13761  eqgen  13764  ecqusaddcl  13776  ghmrn  13794  ghmnsgima  13805  conjsubg  13814  conjnmz  13816  ring1  14022  dvdsrvald  14057  dvdsrd  14058  dvdsrex  14062  0unit  14093  invrpropdg  14113  lringuplu  14160  subrngin  14177  subsubrng  14178  subrgcrng  14189  subrgin  14208  subsubrg  14209  islmodd  14257  lssvacl  14329  lssvancl1  14331  lss0cl  14333  lssvscl  14339  lssvnegcl  14340  lssincl  14349  issubrgd  14416  lidlrsppropdg  14459  2idlcpblrng  14487  zsssubrg  14549  unopn  14679  tsettps  14712  tgss2  14753  difopn  14782  resttop  14844  resttopon  14845  restco  14848  tgcn  14882  tgcnp  14883  cnptopco  14896  upxp  14946  txcn  14949  txdis  14951  cnmpt11  14957  cnmpt11f  14958  cnmpt1t  14959  cnmpt12  14961  cnmpt21  14965  cnmpt21f  14966  cnmpt2t  14967  cnmpt22  14968  cnmpt22f  14969  cnmpt1res  14970  xmeter  15110  mscl  15139  xmscl  15140  bdxmet  15175  cncfmpt1f  15272  cdivcncfap  15278  negfcncf  15280  ivthreinc  15319  cnmptlimc  15348  dvcnp2cntop  15373  elplyd  15415  plypow  15418  plyconst  15419  plyaddlem1  15421  plysub  15427  dvply2g  15440  sincn  15443  coscn  15444  relogcl  15536  mpodvdsmulf1o  15664  fsumdvdsmul  15665  mersenne  15671  perfect  15675  lgsne0  15717  lgseisenlem4  15752  lgsquadlem1  15756  pwtrufal  16363