Theorem eqeltrrd 2255

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr3d  2260  exmid01  4197  pwntru  4198  xpexr2m  5069  funimaexg  5299  fvmptdv2  5604  ffvresb  5678  2ndrn  6181  1st2ndbr  6182  elopabi  6193  cnvf1olem  6222  dftpos4  6261  tfrlemibxssdm  6325  tfr1onlembxssdm  6341  tfrcllembxssdm  6354  nnmordi  6514  th3qlem1  6634  infiexmid  6874  onunsnss  6913  ssfirab  6930  ssfidc  6931  fnfi  6933  fidcenumlemr  6951  elfi2  6968  ordiso2  7031  djulclb  7051  ctmlemr  7104  ctssdccl  7107  ctssdc  7109  exmidfodomrlemreseldju  7196  exmidfodomrlemr  7198  exmidapne  7256  archnqq  7413  prarloclemarch2  7415  enq0tr  7430  nqnq0  7437  addcmpblnq0  7439  mulcmpblnq0  7440  mulcanenq0ec  7441  addclnq0  7447  mulclnq0  7448  nqpnq0nq  7449  nq0m0r  7452  distrnq0  7455  addassnq0lemcl  7457  prarloclemlt  7489  prarloclem5  7496  distrlem4prl  7580  distrlem4pru  7581  ltexprlemm  7596  ltexprlemrl  7606  ltexprlemru  7608  addcanprleml  7610  cauappcvgprlemladdru  7652  prsrlem1  7738  mulgt0sr  7774  axpre-suploclemres  7897  cnegexlem2  8129  subf  8155  resubcl  8217  negcon1ad  8259  subeq0bd  8332  rimul  8538  rereim  8539  aprcl  8599  nn0nnaddcl  9203  elnn0nn  9214  zaddcllemneg  9288  zsubcl  9290  zrevaddcl  9299  elz2  9320  zdiv  9337  peano5uzti  9357  peano2uzr  9581  uzaddcl  9582  divfnzn  9617  qsubcl  9634  qrevaddcl  9640  fseq1p1m1  10089  modqmuladdim  10362  frec2uzrand  10400  frecuzrdglem  10406  frecuzrdg0  10408  frecuzrdgdomlem  10412  frecuzrdg0t  10417  frecuzrdgsuctlem  10418  seq3val  10453  seq3feq  10467  iseqf1olemnab  10483  seqfeq3  10507  expaddzaplem  10558  expaddzap  10559  expmulzap  10561  zesq  10633  bcm1k  10733  bccl  10740  permnn  10744  seq3coll  10815  shftuz  10819  ref  10857  imf  10858  crre  10859  rereb  10865  resqrexlemnm  11020  absf  11112  summodclem2a  11382  summodc  11384  fsumgcl  11387  fsum3  11388  fsumf1o  11391  fsumcnv  11438  mptfzshft  11443  isumlessdc  11497  geolim2  11513  prodmodclem3  11576  fprodseq  11584  fprodf1o  11589  oexpneg  11874  nn0ob  11905  divalglemqt  11916  suprzubdc  11945  gcdf  11965  lcmgcdlem  12069  sqnprm  12128  sqrt2irrlem  12153  2sqpwodd  12168  fnum  12182  fden  12183  phimullem  12217  pc2dvds  12321  gzsubcl  12370  4sqlem5  12372  4sqlem9  12376  4sqlem10  12377  mul4sqlem  12383  mul4sq  12384  ctiunctlemfo  12432  mgmsscl  12712  mhmima  12807  mhmmnd  12912  mulgdir  12946  subgmulg  12979  issubg2m  12980  issubgrpd2  12981  grpissubg  12985  subsubg  12988  isnsg3  12998  ssnmz  13002  eqger  13014  eqgen  13017  ring1  13167  reldvdsrsrg  13192  dvdsrvald  13193  dvdsrd  13194  dvdsrex  13198  0unit  13229  invrpropdg  13249  lringuplu  13268  subrgcrng  13284  subrgin  13303  subsubrg  13304  zsssubrg  13348  unopn  13374  tsettps  13407  tgss2  13450  difopn  13479  resttop  13541  resttopon  13542  restco  13545  tgcn  13579  tgcnp  13580  cnptopco  13593  upxp  13643  txcn  13646  txdis  13648  cnmpt11  13654  cnmpt11f  13655  cnmpt1t  13656  cnmpt12  13658  cnmpt21  13662  cnmpt21f  13663  cnmpt2t  13664  cnmpt22  13665  cnmpt22f  13666  cnmpt1res  13667  xmeter  13807  mscl  13836  xmscl  13837  bdxmet  13872  cncfmpt1f  13955  cdivcncfap  13958  negfcncf  13960  cnmptlimc  14014  dvcnp2cntop  14034  sincn  14061  coscn  14062  relogcl  14154  lgsne0  14310  pwtrufal  14607