Theorem eqeltrrd 2217

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  3eltr3d  2222  exmid01  4121  pwntru  4122  xpexr2m  4980  funimaexg  5207  fvmptdv2  5510  ffvresb  5583  2ndrn  6081  1st2ndbr  6082  elopabi  6093  cnvf1olem  6121  dftpos4  6160  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  nnmordi  6412  th3qlem1  6531  infiexmid  6771  onunsnss  6805  ssfirab  6822  ssfidc  6823  fnfi  6825  fidcenumlemr  6843  elfi2  6860  ordiso2  6920  djulclb  6940  ctmlemr  6993  ctssdccl  6996  ctssdc  6998  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  archnqq  7225  prarloclemarch2  7227  enq0tr  7242  nqnq0  7249  addcmpblnq0  7251  mulcmpblnq0  7252  mulcanenq0ec  7253  addclnq0  7259  mulclnq0  7260  nqpnq0nq  7261  nq0m0r  7264  distrnq0  7267  addassnq0lemcl  7269  prarloclemlt  7301  prarloclem5  7308  distrlem4prl  7392  distrlem4pru  7393  ltexprlemm  7408  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  cauappcvgprlemladdru  7464  prsrlem1  7550  mulgt0sr  7586  axpre-suploclemres  7709  cnegexlem2  7938  subf  7964  resubcl  8026  negcon1ad  8068  subeq0bd  8141  rimul  8347  rereim  8348  aprcl  8408  nn0nnaddcl  9008  elnn0nn  9019  zaddcllemneg  9093  zsubcl  9095  zrevaddcl  9104  elz2  9122  zdiv  9139  peano5uzti  9159  peano2uzr  9380  uzaddcl  9381  divfnzn  9413  qsubcl  9430  qrevaddcl  9436  fseq1p1m1  9874  modqmuladdim  10140  frec2uzrand  10178  frecuzrdglem  10184  frecuzrdg0  10186  frecuzrdgdomlem  10190  frecuzrdg0t  10195  frecuzrdgsuctlem  10196  seq3val  10231  seq3feq  10245  iseqf1olemnab  10261  seqfeq3  10285  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  zesq  10410  bcm1k  10506  bccl  10513  permnn  10517  seq3coll  10585  shftuz  10589  ref  10627  imf  10628  crre  10629  rereb  10635  resqrexlemnm  10790  absf  10882  summodclem2a  11150  summodc  11152  fsumgcl  11155  fsum3  11156  fsumf1o  11159  fsumcnv  11206  mptfzshft  11211  isumlessdc  11265  geolim2  11281  prodmodclem3  11344  oexpneg  11574  nn0ob  11605  divalglemqt  11616  gcdf  11661  lcmgcdlem  11758  sqnprm  11816  sqrt2irrlem  11839  2sqpwodd  11854  fnum  11868  fden  11869  phimullem  11901  ctiunctlemfo  11952  unopn  12172  tsettps  12205  tgss2  12248  difopn  12277  resttop  12339  resttopon  12340  restco  12343  tgcn  12377  tgcnp  12378  cnptopco  12391  upxp  12441  txcn  12444  txdis  12446  cnmpt11  12452  cnmpt11f  12453  cnmpt1t  12454  cnmpt12  12456  cnmpt21  12460  cnmpt21f  12461  cnmpt2t  12462  cnmpt22  12463  cnmpt22f  12464  cnmpt1res  12465  xmeter  12605  mscl  12634  xmscl  12635  bdxmet  12670  cncfmpt1f  12753  cdivcncfap  12756  negfcncf  12758  cnmptlimc  12812  dvcnp2cntop  12832  sincn  12858  coscn  12859  pwtrufal  13192