Theorem eqeltrd 2311

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)

Hypotheses

Ref	Expression
eqeltrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrd.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
2		eqeltrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	eleq1d 2303	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eqeltrrd  2312  3eltr4d  2318  eqeltrid  2321  eqeltrdi  2325  ifcldadc  3656  ifcldcd  3664  intab  3983  disjiun  4109  iinexgm  4271  opexg  4349  tfisi  4714  nnpredcl  4750  opabssxpd  4791  imain  5443  fvmptd  5763  fvmptdf  5770  fvmptt  5774  elfvmptrab  5778  dffo3  5829  resfunexg  5910  f1oiso2  6006  riota2df  6033  riota5f  6038  ovmpodxf  6187  ovmpodf  6193  offval  6283  ofvalg  6285  offeq  6289  iunexg  6321  oprabexd  6333  fo1stresm  6368  fo2ndresm  6369  oprssdmm  6378  1stdm  6389  1stconst  6430  2ndconst  6431  cnvf1olem  6433  fo2ndf  6436  f1od2  6444  iunon  6528  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  tfrcl  6608  rdgon  6630  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  oacl  6706  omcl  6707  oeicl  6708  nntr2  6749  mptelixpg  6982  fidifsnen  7138  en2eqpr  7180  unfiin  7199  tpfidceq  7203  ssfirab  7210  fnfi  7216  relcnvfi  7221  fidcenumlemr  7238  snopfsuppdc  7265  fsuppcorn  7267  elfi2  7272  supclti  7302  supubti  7303  suplubti  7304  supelti  7306  ordiso2  7339  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djuss  7374  updjudhcoinlf  7384  updjudhcoinrg  7385  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nninfwlpoimlemg  7479  cardcl  7490  exmidontriimlem2  7542  exmidapne  7590  cc2lem  7596  cc3  7598  addclpi  7658  mulclpi  7659  addclnq  7706  mulclnq  7707  addclnq0  7782  mulclnq0  7783  nqpnq0nq  7784  elnp1st2nd  7807  prarloclemcalc  7833  distrlem1prl  7913  distrlem1pru  7914  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  addcanprlemu  7946  recexprlemloc  7962  aptiprleml  7970  caucvgprprlemopl  8028  suplocexprlemex  8053  addclsr  8084  mulclsr  8085  recexgt0sr  8104  mulextsr1lem  8111  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axaddcl  8195  axaddrcl  8196  axmulcl  8197  axmulrcl  8198  axcaucvglemval  8228  subcl  8488  cru  8893  aprcl  8937  aptap  8941  divclap  8969  redivclap  9022  diveqap1bd  9127  lbinfcl  9240  cju  9252  nn1m1nn  9272  nnsub  9293  nnnn0addcl  9543  un0addcl  9546  peano2z  9630  peano2zm  9632  zaddcllemneg  9633  zaddcl  9634  nnaddm1cl  9656  nn0n0n1ge2  9665  zdivadd  9685  zdivmul  9686  suprzclex  9694  zneo  9697  peano5uzti  9704  supinfneg  9945  infsupneg  9946  qmulz  9973  qnegcl  9986  qapne  9989  qdivcl  9993  cnref1o  10001  xnegcl  10184  xltnegi  10187  xaddnemnf  10209  xaddnepnf  10210  xnegdi  10220  xnpcan  10224  xltadd1  10228  xposdif  10234  xleaddadd  10239  iccf1o  10357  ige3m2fz  10403  ige2m1fz1  10465  zssinfcl  10614  infssuzex  10615  infssuzcldc  10617  zsupssdc  10622  suprzcl2dc  10623  rebtwn2z  10638  flqcl  10657  flapcl  10659  ceilqcl  10694  intfracq  10706  modqcl  10712  mulqmod0  10716  modqdifz  10722  zmodcl  10730  modfzo0difsn  10781  modsumfzodifsn  10782  frec2uzzd  10786  frec2uzsucd  10787  frec2uzuzd  10788  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgsuctlem  10809  fzofig  10818  iseqovex  10844  seq3val  10846  seqvalcd  10847  seqf  10850  seqovcd  10853  seq3clss  10857  seq3caopr3  10877  iseqf1olemnab  10887  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem2a  10904  seqf1oglem1  10905  seqf1oglem2  10906  seq3distr  10918  ser0f  10920  ser3le  10923  exp3vallem  10926  exp3val  10927  exp1  10931  expcl2lemap  10937  m1expcl2  10947  expaddzap  10969  sqcl  10986  nnsqcl  10995  qsqcl  10997  zesq  11045  facp1  11117  faccl  11122  facdiv  11125  bcval  11136  bcrpcl  11140  bcp1n  11148  bcpasc  11153  permnn  11159  hashennn  11168  hashcl  11169  lencl  11253  wrdexg  11260  elovmpowrd  11291  lswcl  11300  ccatcl  11306  ccatrn  11322  lswccatn0lsw  11324  ccatalpha  11326  s1cl  11334  swrdclg  11367  swrdwrdsymbg  11381  ccatswrd  11387  pfxval  11391  fnpfx  11394  pfxclg  11395  pfxwrdsymbg  11407  ccatpfx  11418  lenrevpfxcctswrd  11429  wrdind  11439  wrd2ind  11440  shftlem  11526  ovshftex  11529  shftf  11540  seq3shft  11548  cjth  11556  imval  11560  recl  11563  imcl  11564  crre  11567  remim  11570  reim0b  11572  cvg1nlemcau  11694  uzin2  11697  resqrexlem1arp  11715  resqrexlemp1rp  11716  resqrexlemglsq  11732  resqrexlemga  11733  resqrtcl  11739  abscl  11761  absrpclap  11771  nn0abscl  11795  fzomaxdiflem  11822  fzomaxdif  11823  maxabslemab  11916  maxcl  11920  zmaxcl  11934  minmax  11940  mincl  11941  xrmaxcl  11962  xrmaxaddlem  11970  xrminmax  11975  xrmincl  11976  xrmineqinf  11979  xrminrpcl  11984  reccn2ap  12023  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  climle  12044  climlec2  12051  climcvg1nlem  12059  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumgcl  12097  fsum3  12098  isumss  12102  fisumss  12103  isumss2  12104  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumcllem  12110  fsumadd  12117  sumsnf  12120  fsumsplitsn  12121  isumcl  12136  isummulc2  12137  isumrecl  12140  isumge0  12141  isumadd  12142  fsum2dlemstep  12145  fisumcom2  12149  mptfzshft  12153  fsumrev  12154  fsummulc2  12159  iserabs  12186  isumshft  12201  isumsplit  12202  isum1p  12203  isumrpcl  12205  isumle  12206  isumlessdc  12207  trireciplem  12211  expcnvap0  12213  expcnvre  12214  expcnv  12215  explecnv  12216  geolim  12222  geolim2  12223  geo2lim  12227  cvgratnnlemsumlt  12239  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodf1f  12254  prodfdivap  12258  prodrbdclem  12282  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prodssdc  12300  fprodmul  12302  prodsnf  12303  fprodsplitdc  12307  fprodunsn  12315  fprodcl2lem  12316  fprodcllem  12317  fprodabs  12327  fprodrev  12330  fprod2dlemstep  12333  fprodcom2fi  12337  fprodsplitsn  12344  efcllemp  12369  ef0lem  12371  efcvgfsum  12378  reefcl  12379  ege2le3  12382  efcj  12384  efaddlem  12385  eftlcvg  12398  eftlcl  12399  reeftlcl  12400  eftlub  12401  efsep  12402  effsumlt  12403  efgt1p2  12406  efgt1p  12407  reeff1  12411  tanclap  12420  resincl  12431  recoscl  12432  retanclap  12433  eirraplem  12488  dvdsval2  12501  fsumdvds  12553  sqoddm1div8z  12597  bitsinv1lem  12672  gcdval  12680  gcdn0cl  12683  gcddvds  12684  divgcdnnr  12697  uzwodc  12758  nn0seqcvgd  12763  ialgrlem1st  12764  ialgrlemconst  12765  algrf  12767  algrp1  12768  eucalgf  12777  eucalglt  12779  lcmval  12785  lcmcllem  12789  lcmgcdlem  12799  cncongr2  12826  sqrt2irrlem  12883  oddpwdclemxy  12891  oddpwdclemdc  12895  qden1elz  12927  phicl2  12936  phimullem  12947  eulerthlemth  12954  prmdiv  12957  odzcllem  12965  pythagtriplem8  12995  pythagtriplem9  12996  pcval  13019  pczcl  13021  pcqcl  13029  dvdsprmpweqle  13060  pcaddlem  13062  pcmptcl  13065  pcmpt  13066  pockthlem  13079  pockthg  13080  zgz  13096  gznegcl  13098  gzcjcl  13099  gzaddcl  13100  gzmulcl  13101  gzabssqcl  13104  4sqlem5  13105  4sqlem4a  13114  mul4sqlem  13116  mul4sq  13117  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  4sqexercise1  13121  4sqlem16  13129  4sqlem17  13130  ballotfilemfelz  13174  ballotfilemiex  13188  ballotfilemsdom  13199  ballotfilemgval  13211  ennnfonelemjn  13237  ennnfonelemg  13238  ennnfonelemp1  13241  ctinfomlemom  13262  ctiunctlemfo  13274  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  setsex  13328  strsetsid  13329  strslfv3  13342  bassetsnn  13353  ressex  13362  ressbas2d  13365  strressid  13368  tgvalex  13560  ptex  13561  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfn  13581  imasaddval  13582  imasaddf  13583  imasmulfn  13584  imasmulval  13585  imasmulf  13586  qusval  13587  qusex  13589  qusaddvallemg  13597  qusaddflemg  13598  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  mgm1  13633  gsumress  13658  gsumprval  13662  mhmex  13717  subsubm  13738  0subm  13739  mhmeql  13747  gsumwsubmcl  13751  gsumfzcl  13754  grpsubval  13801  grplinv  13805  qusgrp2  13866  mulgval  13875  mulgex  13876  mulgfng  13877  mulg1  13882  mulgnnp1  13883  mulgnnsubcl  13887  mulgnn0subcl  13888  mulgsubcl  13889  mulgnndir  13904  subgex  13929  subgsubcl  13938  issubgrpd  13944  subsubg  13950  nsgconj  13959  0nsg  13967  triv1nsgd  13971  eqgex  13974  eqger  13977  eqgcpbl  13981  ghmex  14008  ghmpreima  14019  ghmnsgpreima  14022  conjnmz  14032  gsumfzsubmcl  14091  gsumsplit0  14099  gfsumval  14102  gfsumsn  14107  gfsumcl  14110  prdsex  14114  prdsval  14115  prdsplusgsgrpcl  14132  prdsplusgcl  14134  prdsidlem  14135  pwsmnd  14154  pwsgrp  14156  mgpex  14164  rngmgpf  14176  qusrng  14197  mgpf  14254  qusring2  14309  opprex  14316  opprrng  14320  opprring  14322  dvdsrex  14343  opprunitd  14355  dvrvald  14379  dvrcl  14380  unitdvcl  14381  invrpropdg  14394  subsubrng  14460  subrgcrng  14471  subrgsubm  14480  subrgugrp  14486  subsubrg  14491  rnrhmsubrg  14498  aprcotr  14535  aprnzr  14537  aprlring  14538  rmodislmod  14625  lssvsubcl  14640  islss3  14653  lspex  14669  ellspsn  14691  sraex  14720  rlmlmod  14738  lidlex  14747  rspex  14748  lidl0cl  14757  lidlacl  14758  lidlnegcl  14759  ridl0  14784  ridl1  14785  2idlelbas  14790  cnsubglem  14853  expghmap  14881  mulgrhm  14883  zrhex  14895  znbaslemnn  14913  psrval  14940  psrbagfi  14949  psrbagcon  14952  psrbasg  14955  mplsubgfilemm  14979  mplsubgfilemcl  14980  mplsubgfileminv  14981  mplgrpfi  14987  iunopn  14993  toponmax  15016  tgtop  15059  tgiun  15064  tgidm  15065  ntropn  15108  tgrest  15160  restopnb  15172  cnovex  15187  cnclima  15214  txvalex  15245  txtop  15251  tx1cn  15260  tx2cn  15261  txcnp  15262  txcnmpt  15264  txdis1cn  15269  cnmptcom  15289  imasnopn  15290  hmeocnv  15298  hmeores  15306  txhmeo  15310  txswaphmeo  15312  ispsmet  15314  xmetres  15373  metres  15374  blex  15378  xmeter  15427  xmetresbl  15431  mopntopon  15434  isxms2  15443  xmetxp  15498  xmettx  15501  txmetcnp  15509  qtopbasss  15512  qtopbas  15513  reopnap  15537  ioo2blex  15543  blssioo  15544  tgioo  15545  fsumcncntop  15558  expcn  15560  cncfval  15563  divccncfap  15581  cdivcncfap  15595  divcncfap  15605  maxcncf  15606  mincncf  15607  ivthdec  15635  hoverb  15639  limccnpcntop  15666  dvrecap  15704  elplyd  15732  ply1termlem  15733  ply1term  15734  plymullem1  15739  plyaddlem  15740  plymullem  15741  plycolemc  15749  plyco  15750  plycj  15752  plycn  15753  plyreres  15755  dvply1  15756  dvply2g  15757  pilem3  15774  tanrpcl  15828  cosordlem  15840  ioocosf1o  15845  rpcncxpcl  15893  rpcxpcl  15894  rpabscxpbnd  15931  rplogbcl  15937  pellexlem1  15971  sgmnncl  15982  mpodvdsmulf1o  15984  fsumdvdsmul  15985  mersenne  15991  perfectlem2  15994  lgslem1  15999  lgsval  16003  lgscllem  16006  lgsne0  16037  gausslemma2dlem4  16063  lgseisenlem1  16069  lgsquadlem1  16076  lgsquadlem2  16077  2sqlem3  16116  2sqlem8  16122  vtxex  16139  iedgex  16140  edgvalg  16180  edgopval  16183  edgstruct  16185  usgrausgrien  16290  ausgrumgrien  16291  ausgrusgrien  16292  uspgr1ewopdc  16365  usgr2v1e2w  16367  uhgrspansubgrlem  16397  vtxdgfif  16414  vtxdfifiun  16418  1loopgrvd2fi  16426  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  p1evtxdeqfilem  16432  vdegp1bid  16436  wlkex  16446  wlkelvv  16470  clwwlkccat  16522  clwwlknonex2lem1  16558  clwwlknonex2lem2  16559  clwwlknonex2  16560  trlsegvdeglem6  16586  trlsegvdeglem7  16587  trlsegvdegfi  16588  eupth2lem3lem1fi  16589  eupth2lem3lem2fi  16590  eupth2lem3lem5  16593  eupth2lembfi  16598  eulerpathprum  16601  depindlem1  16627  depindlem2  16628  djucllem  16698  012of  16893  2o01f  16894  nninfsellemeq  16918  qdencn  16933  cvgcmp2nlemabs  16942  trilpolemclim  16946  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  nconstwlpolemgt0  16976