Theorem eqeltrrd 2242

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

Syntax hints:   → wi 4   = wceq 1342   ∈ wcel 2135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160

This theorem is referenced by:  3eltr3d  2247  exmid01  4171  pwntru  4172  xpexr2m  5039  funimaexg  5266  fvmptdv2  5569  ffvresb  5642  2ndrn  6143  1st2ndbr  6144  elopabi  6155  cnvf1olem  6183  dftpos4  6222  tfrlemibxssdm  6286  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  nnmordi  6475  th3qlem1  6594  infiexmid  6834  onunsnss  6873  ssfirab  6890  ssfidc  6891  fnfi  6893  fidcenumlemr  6911  elfi2  6928  ordiso2  6991  djulclb  7011  ctmlemr  7064  ctssdccl  7067  ctssdc  7069  exmidfodomrlemreseldju  7147  exmidfodomrlemr  7149  archnqq  7349  prarloclemarch2  7351  enq0tr  7366  nqnq0  7373  addcmpblnq0  7375  mulcmpblnq0  7376  mulcanenq0ec  7377  addclnq0  7383  mulclnq0  7384  nqpnq0nq  7385  nq0m0r  7388  distrnq0  7391  addassnq0lemcl  7393  prarloclemlt  7425  prarloclem5  7432  distrlem4prl  7516  distrlem4pru  7517  ltexprlemm  7532  ltexprlemrl  7542  ltexprlemru  7544  addcanprleml  7546  cauappcvgprlemladdru  7588  prsrlem1  7674  mulgt0sr  7710  axpre-suploclemres  7833  cnegexlem2  8065  subf  8091  resubcl  8153  negcon1ad  8195  subeq0bd  8268  rimul  8474  rereim  8475  aprcl  8535  nn0nnaddcl  9136  elnn0nn  9147  zaddcllemneg  9221  zsubcl  9223  zrevaddcl  9232  elz2  9253  zdiv  9270  peano5uzti  9290  peano2uzr  9514  uzaddcl  9515  divfnzn  9550  qsubcl  9567  qrevaddcl  9573  fseq1p1m1  10019  modqmuladdim  10292  frec2uzrand  10330  frecuzrdglem  10336  frecuzrdg0  10338  frecuzrdgdomlem  10342  frecuzrdg0t  10347  frecuzrdgsuctlem  10348  seq3val  10383  seq3feq  10397  iseqf1olemnab  10413  seqfeq3  10437  expaddzaplem  10488  expaddzap  10489  expmulzap  10491  zesq  10562  bcm1k  10662  bccl  10669  permnn  10673  seq3coll  10741  shftuz  10745  ref  10783  imf  10784  crre  10785  rereb  10791  resqrexlemnm  10946  absf  11038  summodclem2a  11308  summodc  11310  fsumgcl  11313  fsum3  11314  fsumf1o  11317  fsumcnv  11364  mptfzshft  11369  isumlessdc  11423  geolim2  11439  prodmodclem3  11502  fprodseq  11510  fprodf1o  11515  oexpneg  11799  nn0ob  11830  divalglemqt  11841  suprzubdc  11870  gcdf  11890  lcmgcdlem  11988  sqnprm  12047  sqrt2irrlem  12070  2sqpwodd  12085  fnum  12099  fden  12100  phimullem  12134  pc2dvds  12238  ctiunctlemfo  12309  unopn  12544  tsettps  12577  tgss2  12620  difopn  12649  resttop  12711  resttopon  12712  restco  12715  tgcn  12749  tgcnp  12750  cnptopco  12763  upxp  12813  txcn  12816  txdis  12818  cnmpt11  12824  cnmpt11f  12825  cnmpt1t  12826  cnmpt12  12828  cnmpt21  12832  cnmpt21f  12833  cnmpt2t  12834  cnmpt22  12835  cnmpt22f  12836  cnmpt1res  12837  xmeter  12977  mscl  13006  xmscl  13007  bdxmet  13042  cncfmpt1f  13125  cdivcncfap  13128  negfcncf  13130  cnmptlimc  13184  dvcnp2cntop  13204  sincn  13231  coscn  13232  relogcl  13324  pwtrufal  13711