Theorem eqeltrrd 2283

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  3eltr3d  2288  exmid01  4242  pwntru  4243  xpexr2m  5124  funimaexg  5358  fvmptdv2  5669  ffvresb  5743  iotaexel  5904  2ndrn  6269  1st2ndbr  6270  elopabi  6281  cnvf1olem  6310  dftpos4  6349  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  nnmordi  6602  th3qlem1  6724  infiexmid  6974  onunsnss  7014  ssfirab  7033  ssfidc  7034  fnfi  7038  fidcenumlemr  7057  elfi2  7074  ordiso2  7137  djulclb  7157  ctmlemr  7210  ctssdccl  7213  ctssdc  7215  exmidfodomrlemreseldju  7308  exmidfodomrlemr  7310  exmidapne  7372  archnqq  7530  prarloclemarch2  7532  enq0tr  7547  nqnq0  7554  addcmpblnq0  7556  mulcmpblnq0  7557  mulcanenq0ec  7558  addclnq0  7564  mulclnq0  7565  nqpnq0nq  7566  nq0m0r  7569  distrnq0  7572  addassnq0lemcl  7574  prarloclemlt  7606  prarloclem5  7613  distrlem4prl  7697  distrlem4pru  7698  ltexprlemm  7713  ltexprlemrl  7723  ltexprlemru  7725  addcanprleml  7727  cauappcvgprlemladdru  7769  prsrlem1  7855  mulgt0sr  7891  axpre-suploclemres  8014  cnegexlem2  8248  subf  8274  resubcl  8336  negcon1ad  8378  subeq0bd  8451  rimul  8658  rereim  8659  aprcl  8719  nn0nnaddcl  9326  elnn0nn  9337  zaddcllemneg  9411  zsubcl  9413  zrevaddcl  9423  elz2  9444  zdiv  9461  peano5uzti  9481  peano2uzr  9706  uzaddcl  9707  divfnzn  9742  qsubcl  9759  qrevaddcl  9765  fseq1p1m1  10216  suprzubdc  10379  modqmuladdim  10512  frec2uzrand  10550  frecuzrdglem  10556  frecuzrdg0  10558  frecuzrdgdomlem  10562  frecuzrdg0t  10567  frecuzrdgsuctlem  10568  seq3val  10605  seq3feq  10625  iseqf1olemnab  10646  seqf1oglem2  10665  seqfeq3  10674  seqfeq4g  10676  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  zesq  10803  bcm1k  10905  bccl  10912  permnn  10916  seq3coll  10987  ccatrn  11065  shftuz  11128  ref  11166  imf  11167  crre  11168  rereb  11174  resqrexlemnm  11329  absf  11421  summodclem2a  11692  summodc  11694  fsumgcl  11697  fsum3  11698  fsumf1o  11701  fsumcnv  11748  mptfzshft  11753  isumlessdc  11807  geolim2  11823  prodmodclem3  11886  fprodseq  11894  fprodf1o  11899  dvdsaddre2b  12152  3dvds  12175  oexpneg  12188  nn0ob  12219  divalglemqt  12230  gcdf  12293  lcmgcdlem  12399  sqnprm  12458  sqrt2irrlem  12483  2sqpwodd  12498  fnum  12512  fden  12513  phimullem  12547  pc2dvds  12653  gzsubcl  12703  4sqlem5  12705  4sqlem9  12709  4sqlem10  12710  mul4sqlem  12716  mul4sq  12717  4sqlem11  12724  4sqlem13m  12726  4sqlem16  12729  4sqlem17  12730  4sqlem18  12731  ctiunctlemfo  12810  ptex  13096  prdsval  13105  prdsbas  13108  prdsbascl  13121  mgmsscl  13193  subsubm  13315  mhmima  13323  imasgrp2  13446  mhmmnd  13452  mulgdir  13490  subgmulg  13524  issubg2m  13525  issubgrpd2  13526  grpissubg  13530  subsubg  13533  isnsg3  13543  ssnmz  13547  eqger  13560  eqgen  13563  ecqusaddcl  13575  ghmrn  13593  ghmnsgima  13604  conjsubg  13613  conjnmz  13615  ring1  13821  reldvdsrsrg  13854  dvdsrvald  13855  dvdsrd  13856  dvdsrex  13860  0unit  13891  invrpropdg  13911  lringuplu  13958  subrngin  13975  subsubrng  13976  subrgcrng  13987  subrgin  14006  subsubrg  14007  islmodd  14055  lssvacl  14127  lssvancl1  14129  lss0cl  14131  lssvscl  14137  lssvnegcl  14138  lssincl  14147  issubrgd  14214  lidlrsppropdg  14257  2idlcpblrng  14285  zsssubrg  14347  unopn  14477  tsettps  14510  tgss2  14551  difopn  14580  resttop  14642  resttopon  14643  restco  14646  tgcn  14680  tgcnp  14681  cnptopco  14694  upxp  14744  txcn  14747  txdis  14749  cnmpt11  14755  cnmpt11f  14756  cnmpt1t  14757  cnmpt12  14759  cnmpt21  14763  cnmpt21f  14764  cnmpt2t  14765  cnmpt22  14766  cnmpt22f  14767  cnmpt1res  14768  xmeter  14908  mscl  14937  xmscl  14938  bdxmet  14973  cncfmpt1f  15070  cdivcncfap  15076  negfcncf  15078  ivthreinc  15117  cnmptlimc  15146  dvcnp2cntop  15171  elplyd  15213  plypow  15216  plyconst  15217  plyaddlem1  15219  plysub  15225  dvply2g  15238  sincn  15241  coscn  15242  relogcl  15334  mpodvdsmulf1o  15462  fsumdvdsmul  15463  mersenne  15469  perfect  15473  lgsne0  15515  lgseisenlem4  15550  lgsquadlem1  15554  pwtrufal  15934