Theorem eqeltrrd 2248

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  3eltr3d  2253  exmid01  4184  pwntru  4185  xpexr2m  5052  funimaexg  5282  fvmptdv2  5585  ffvresb  5659  2ndrn  6162  1st2ndbr  6163  elopabi  6174  cnvf1olem  6203  dftpos4  6242  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  nnmordi  6495  th3qlem1  6615  infiexmid  6855  onunsnss  6894  ssfirab  6911  ssfidc  6912  fnfi  6914  fidcenumlemr  6932  elfi2  6949  ordiso2  7012  djulclb  7032  ctmlemr  7085  ctssdccl  7088  ctssdc  7090  exmidfodomrlemreseldju  7177  exmidfodomrlemr  7179  archnqq  7379  prarloclemarch2  7381  enq0tr  7396  nqnq0  7403  addcmpblnq0  7405  mulcmpblnq0  7406  mulcanenq0ec  7407  addclnq0  7413  mulclnq0  7414  nqpnq0nq  7415  nq0m0r  7418  distrnq0  7421  addassnq0lemcl  7423  prarloclemlt  7455  prarloclem5  7462  distrlem4prl  7546  distrlem4pru  7547  ltexprlemm  7562  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  cauappcvgprlemladdru  7618  prsrlem1  7704  mulgt0sr  7740  axpre-suploclemres  7863  cnegexlem2  8095  subf  8121  resubcl  8183  negcon1ad  8225  subeq0bd  8298  rimul  8504  rereim  8505  aprcl  8565  nn0nnaddcl  9166  elnn0nn  9177  zaddcllemneg  9251  zsubcl  9253  zrevaddcl  9262  elz2  9283  zdiv  9300  peano5uzti  9320  peano2uzr  9544  uzaddcl  9545  divfnzn  9580  qsubcl  9597  qrevaddcl  9603  fseq1p1m1  10050  modqmuladdim  10323  frec2uzrand  10361  frecuzrdglem  10367  frecuzrdg0  10369  frecuzrdgdomlem  10373  frecuzrdg0t  10378  frecuzrdgsuctlem  10379  seq3val  10414  seq3feq  10428  iseqf1olemnab  10444  seqfeq3  10468  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  zesq  10594  bcm1k  10694  bccl  10701  permnn  10705  seq3coll  10777  shftuz  10781  ref  10819  imf  10820  crre  10821  rereb  10827  resqrexlemnm  10982  absf  11074  summodclem2a  11344  summodc  11346  fsumgcl  11349  fsum3  11350  fsumf1o  11353  fsumcnv  11400  mptfzshft  11405  isumlessdc  11459  geolim2  11475  prodmodclem3  11538  fprodseq  11546  fprodf1o  11551  oexpneg  11836  nn0ob  11867  divalglemqt  11878  suprzubdc  11907  gcdf  11927  lcmgcdlem  12031  sqnprm  12090  sqrt2irrlem  12115  2sqpwodd  12130  fnum  12144  fden  12145  phimullem  12179  pc2dvds  12283  gzsubcl  12332  4sqlem5  12334  4sqlem9  12338  4sqlem10  12339  mul4sqlem  12345  mul4sq  12346  ctiunctlemfo  12394  mgmsscl  12615  mhmima  12706  unopn  12797  tsettps  12830  tgss2  12873  difopn  12902  resttop  12964  resttopon  12965  restco  12968  tgcn  13002  tgcnp  13003  cnptopco  13016  upxp  13066  txcn  13069  txdis  13071  cnmpt11  13077  cnmpt11f  13078  cnmpt1t  13079  cnmpt12  13081  cnmpt21  13085  cnmpt21f  13086  cnmpt2t  13087  cnmpt22  13088  cnmpt22f  13089  cnmpt1res  13090  xmeter  13230  mscl  13259  xmscl  13260  bdxmet  13295  cncfmpt1f  13378  cdivcncfap  13381  negfcncf  13383  cnmptlimc  13437  dvcnp2cntop  13457  sincn  13484  coscn  13485  relogcl  13577  lgsne0  13733  pwtrufal  14030