Theorem eqeltrd 2308

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 2300	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

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 2213

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

This theorem is referenced by:  eqeltrrd  2309  3eltr4d  2315  eqeltrid  2318  eqeltrdi  2322  ifcldadc  3639  ifcldcd  3647  intab  3962  disjiun  4088  iinexgm  4249  opexg  4326  tfisi  4691  nnpredcl  4727  opabssxpd  4768  imain  5419  fvmptd  5736  fvmptdf  5743  fvmptt  5747  elfvmptrab  5751  dffo3  5802  resfunexg  5883  f1oiso2  5978  riota2df  6003  riota5f  6008  ovmpodxf  6157  ovmpodf  6163  offval  6252  ofvalg  6254  offeq  6258  iunexg  6290  oprabexd  6298  fo1stresm  6333  fo2ndresm  6334  oprssdmm  6343  1stdm  6354  1stconst  6395  2ndconst  6396  cnvf1olem  6398  fo2ndf  6401  f1od2  6409  iunon  6493  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembfn  6566  tfrcl  6573  rdgon  6595  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  oacl  6671  omcl  6672  oeicl  6673  nntr2  6714  mptelixpg  6946  fidifsnen  7100  en2eqpr  7142  unfiin  7161  tpfidceq  7165  ssfirab  7172  fnfi  7178  relcnvfi  7183  fidcenumlemr  7197  elfi2  7214  supclti  7240  supubti  7241  suplubti  7242  supelti  7244  ordiso2  7277  djulclr  7291  djurclr  7292  djulcl  7293  djurcl  7294  djuss  7312  updjudhcoinlf  7322  updjudhcoinrg  7323  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  nninfwlpoimlemg  7417  cardcl  7428  exmidontriimlem2  7480  exmidapne  7522  cc2lem  7528  cc3  7530  addclpi  7590  mulclpi  7591  addclnq  7638  mulclnq  7639  addclnq0  7714  mulclnq0  7715  nqpnq0nq  7716  elnp1st2nd  7739  prarloclemcalc  7765  distrlem1prl  7845  distrlem1pru  7846  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  addcanprlemu  7878  recexprlemloc  7894  aptiprleml  7902  caucvgprprlemopl  7960  suplocexprlemex  7985  addclsr  8016  mulclsr  8017  recexgt0sr  8036  mulextsr1lem  8043  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  axaddcl  8127  axaddrcl  8128  axmulcl  8129  axmulrcl  8130  axcaucvglemval  8160  subcl  8420  cru  8824  aprcl  8868  aptap  8872  divclap  8900  redivclap  8953  diveqap1bd  9058  lbinfcl  9171  cju  9183  nn1m1nn  9203  nnsub  9224  nnnn0addcl  9474  un0addcl  9477  peano2z  9559  peano2zm  9561  zaddcllemneg  9562  zaddcl  9563  nnaddm1cl  9585  nn0n0n1ge2  9594  zdivadd  9613  zdivmul  9614  suprzclex  9622  zneo  9625  peano5uzti  9632  supinfneg  9873  infsupneg  9874  qmulz  9901  qnegcl  9914  qapne  9917  qdivcl  9921  cnref1o  9929  xnegcl  10111  xltnegi  10114  xaddnemnf  10136  xaddnepnf  10137  xnegdi  10147  xnpcan  10151  xltadd1  10155  xposdif  10161  xleaddadd  10166  iccf1o  10284  ige3m2fz  10329  ige2m1fz1  10389  zssinfcl  10538  infssuzex  10539  infssuzcldc  10541  zsupssdc  10544  suprzcl2dc  10545  rebtwn2z  10560  flqcl  10579  flapcl  10581  ceilqcl  10616  intfracq  10628  modqcl  10634  mulqmod0  10638  modqdifz  10644  zmodcl  10652  modfzo0difsn  10703  modsumfzodifsn  10704  frec2uzzd  10708  frec2uzsucd  10709  frec2uzuzd  10710  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgg  10724  frecuzrdgsuctlem  10731  fzofig  10740  iseqovex  10766  seq3val  10768  seqvalcd  10769  seqf  10772  seqovcd  10775  seq3clss  10779  seq3caopr3  10799  iseqf1olemnab  10809  iseqf1olemqk  10815  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsum  10821  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem2a  10826  seqf1oglem1  10827  seqf1oglem2  10828  seq3distr  10840  ser0f  10842  ser3le  10845  exp3vallem  10848  exp3val  10849  exp1  10853  expcl2lemap  10859  m1expcl2  10869  expaddzap  10891  sqcl  10908  nnsqcl  10917  qsqcl  10919  zesq  10966  facp1  11038  faccl  11043  facdiv  11046  bcval  11057  bcrpcl  11061  bcp1n  11069  bcpasc  11074  permnn  11079  hashennn  11088  hashcl  11089  lencl  11166  wrdexg  11173  elovmpowrd  11204  lswcl  11213  ccatcl  11219  ccatrn  11235  lswccatn0lsw  11237  ccatalpha  11239  s1cl  11247  swrdclg  11280  swrdwrdsymbg  11294  ccatswrd  11300  pfxval  11304  fnpfx  11307  pfxclg  11308  pfxwrdsymbg  11320  ccatpfx  11331  lenrevpfxcctswrd  11342  wrdind  11352  wrd2ind  11353  shftlem  11439  ovshftex  11442  shftf  11453  seq3shft  11461  cjth  11469  imval  11473  recl  11476  imcl  11477  crre  11480  remim  11483  reim0b  11485  cvg1nlemcau  11607  uzin2  11610  resqrexlem1arp  11628  resqrexlemp1rp  11629  resqrexlemglsq  11645  resqrexlemga  11646  resqrtcl  11652  abscl  11674  absrpclap  11684  nn0abscl  11708  fzomaxdiflem  11735  fzomaxdif  11736  maxabslemab  11829  maxcl  11833  zmaxcl  11847  minmax  11853  mincl  11854  xrmaxcl  11875  xrmaxaddlem  11883  xrminmax  11888  xrmincl  11889  xrmineqinf  11892  xrminrpcl  11897  reccn2ap  11936  climaddc1  11952  climmulc2  11954  climsubc1  11955  climsubc2  11956  climle  11957  climlec2  11964  climcvg1nlem  11972  sumrbdclem  12001  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsumgcl  12010  fsum3  12011  isumss  12015  fisumss  12016  isumss2  12017  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumcllem  12023  fsumadd  12030  sumsnf  12033  fsumsplitsn  12034  isumcl  12049  isummulc2  12050  isumrecl  12053  isumge0  12054  isumadd  12055  fsum2dlemstep  12058  fisumcom2  12062  mptfzshft  12066  fsumrev  12067  fsummulc2  12072  iserabs  12099  isumshft  12114  isumsplit  12115  isum1p  12116  isumrpcl  12118  isumle  12119  isumlessdc  12120  trireciplem  12124  expcnvap0  12126  expcnvre  12127  expcnv  12128  explecnv  12129  geolim  12135  geolim2  12136  geo2lim  12140  cvgratnnlemsumlt  12152  cvgratz  12156  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodf1f  12167  prodfdivap  12171  prodrbdclem  12195  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prodssdc  12213  fprodmul  12215  prodsnf  12216  fprodsplitdc  12220  fprodunsn  12228  fprodcl2lem  12229  fprodcllem  12230  fprodabs  12240  fprodrev  12243  fprod2dlemstep  12246  fprodcom2fi  12250  fprodsplitsn  12257  efcllemp  12282  ef0lem  12284  efcvgfsum  12291  reefcl  12292  ege2le3  12295  efcj  12297  efaddlem  12298  eftlcvg  12311  eftlcl  12312  reeftlcl  12313  eftlub  12314  efsep  12315  effsumlt  12316  efgt1p2  12319  efgt1p  12320  reeff1  12324  tanclap  12333  resincl  12344  recoscl  12345  retanclap  12346  eirraplem  12401  dvdsval2  12414  fsumdvds  12466  sqoddm1div8z  12510  bitsinv1lem  12585  gcdval  12593  gcdn0cl  12596  gcddvds  12597  divgcdnnr  12610  uzwodc  12671  nn0seqcvgd  12676  ialgrlem1st  12677  ialgrlemconst  12678  algrf  12680  algrp1  12681  eucalgf  12690  eucalglt  12692  lcmval  12698  lcmcllem  12702  lcmgcdlem  12712  cncongr2  12739  sqrt2irrlem  12796  oddpwdclemxy  12804  oddpwdclemdc  12808  qden1elz  12840  phicl2  12849  phimullem  12860  eulerthlemth  12867  prmdiv  12870  odzcllem  12878  pythagtriplem8  12908  pythagtriplem9  12909  pcval  12932  pczcl  12934  pcqcl  12942  dvdsprmpweqle  12973  pcaddlem  12975  pcmptcl  12978  pcmpt  12979  pockthlem  12992  pockthg  12993  zgz  13009  gznegcl  13011  gzcjcl  13012  gzaddcl  13013  gzmulcl  13014  gzabssqcl  13017  4sqlem5  13018  4sqlem4a  13027  mul4sqlem  13029  mul4sq  13030  4sqlemafi  13031  4sqlemffi  13032  4sqleminfi  13033  4sqexercise1  13034  4sqlem16  13042  4sqlem17  13043  ennnfonelemjn  13086  ennnfonelemg  13087  ennnfonelemp1  13090  ctinfomlemom  13111  ctiunctlemfo  13123  nninfdclemcl  13132  nninfdclemf  13133  nninfdclemp1  13134  setsex  13177  strsetsid  13178  strslfv3  13191  bassetsnn  13202  ressex  13211  ressbas2d  13214  strressid  13217  tgvalex  13409  ptex  13410  prdsex  13415  prdsval  13419  imasex  13451  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  imasaddfn  13463  imasaddval  13464  imasaddf  13465  imasmulfn  13466  imasmulval  13467  imasmulf  13468  qusval  13469  qusex  13471  qusaddvallemg  13479  qusaddflemg  13480  qusaddval  13481  qusaddf  13482  qusmulval  13483  qusmulf  13484  mgm1  13516  gsumress  13541  gsumprval  13545  prdsplusgsgrpcl  13560  prdsplusgcl  13592  prdsidlem  13593  pwsmnd  13596  mhmex  13608  subsubm  13629  0subm  13630  mhmeql  13638  gsumwsubmcl  13642  gsumfzcl  13645  grpsubval  13692  grplinv  13696  pwsgrp  13757  qusgrp2  13763  mulgval  13772  mulgex  13773  mulgfng  13774  mulg1  13779  mulgnnp1  13780  mulgnnsubcl  13784  mulgnn0subcl  13785  mulgsubcl  13786  mulgnndir  13801  subgex  13826  subgsubcl  13835  issubgrpd  13841  subsubg  13847  nsgconj  13856  0nsg  13864  triv1nsgd  13868  eqgex  13871  eqger  13874  eqgcpbl  13878  ghmex  13905  ghmpreima  13916  ghmnsgpreima  13919  conjnmz  13929  gsumfzsubmcl  13988  gsumsplit0  13996  mgpex  14002  rngmgpf  14014  qusrng  14035  mgpf  14088  qusring2  14143  opprex  14150  opprrng  14154  opprring  14156  dvdsrex  14176  opprunitd  14188  dvrvald  14212  dvrcl  14213  unitdvcl  14214  invrpropdg  14227  subsubrng  14292  subrgcrng  14303  subrgsubm  14312  subrgugrp  14318  subsubrg  14323  rnrhmsubrg  14330  aprcotr  14364  rmodislmod  14430  lssvsubcl  14445  islss3  14458  lspex  14474  ellspsn  14496  sraex  14525  rlmlmod  14543  lidlex  14552  rspex  14553  lidl0cl  14562  lidlacl  14563  lidlnegcl  14564  ridl0  14589  ridl1  14590  2idlelbas  14595  cnsubglem  14658  expghmap  14686  mulgrhm  14688  zrhex  14700  znbaslemnn  14718  psrval  14745  psrbagfi  14753  psrbagcon  14755  psrbasg  14758  mplsubgfilemm  14782  mplsubgfilemcl  14783  mplsubgfileminv  14784  mplgrpfi  14790  iunopn  14796  toponmax  14819  tgtop  14862  tgiun  14867  tgidm  14868  ntropn  14911  tgrest  14963  restopnb  14975  cnovex  14990  cnclima  15017  txvalex  15048  txtop  15054  tx1cn  15063  tx2cn  15064  txcnp  15065  txcnmpt  15067  txdis1cn  15072  cnmptcom  15092  imasnopn  15093  hmeocnv  15101  hmeores  15109  txhmeo  15113  txswaphmeo  15115  ispsmet  15117  xmetres  15176  metres  15177  blex  15181  xmeter  15230  xmetresbl  15234  mopntopon  15237  isxms2  15246  xmetxp  15301  xmettx  15304  txmetcnp  15312  qtopbasss  15315  qtopbas  15316  reopnap  15340  ioo2blex  15346  blssioo  15347  tgioo  15348  fsumcncntop  15361  expcn  15363  cncfval  15366  divccncfap  15384  cdivcncfap  15398  divcncfap  15408  maxcncf  15409  mincncf  15410  ivthdec  15438  hoverb  15442  limccnpcntop  15469  dvrecap  15507  elplyd  15535  ply1termlem  15536  ply1term  15537  plymullem1  15542  plyaddlem  15543  plymullem  15544  plycolemc  15552  plyco  15553  plycj  15555  plycn  15556  plyreres  15558  dvply1  15559  dvply2g  15560  pilem3  15577  tanrpcl  15631  cosordlem  15643  ioocosf1o  15648  rpcncxpcl  15696  rpcxpcl  15697  rpabscxpbnd  15734  rplogbcl  15740  pellexlem1  15774  sgmnncl  15785  mpodvdsmulf1o  15787  fsumdvdsmul  15788  mersenne  15794  perfectlem2  15797  lgslem1  15802  lgsval  15806  lgscllem  15809  lgsne0  15840  gausslemma2dlem4  15866  lgseisenlem1  15872  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem3  15919  2sqlem8  15925  vtxex  15942  iedgex  15943  edgvalg  15983  edgopval  15986  edgstruct  15988  usgrausgrien  16093  ausgrumgrien  16094  ausgrusgrien  16095  uspgr1ewopdc  16168  usgr2v1e2w  16170  uhgrspansubgrlem  16200  vtxdgfif  16217  vtxdfifiun  16221  1loopgrvd2fi  16229  1loopgrvd0fi  16230  1hevtxdg0fi  16231  1hevtxdg1en  16232  p1evtxdeqfilem  16235  vdegp1bid  16239  wlkex  16249  wlkelvv  16273  clwwlkccat  16325  clwwlknonex2lem1  16361  clwwlknonex2lem2  16362  clwwlknonex2  16363  trlsegvdeglem6  16389  trlsegvdeglem7  16390  trlsegvdegfi  16391  eupth2lem3lem1fi  16392  eupth2lem3lem2fi  16393  eupth2lem3lem5  16396  eupth2lembfi  16401  eulerpathprum  16404  depindlem1  16430  depindlem2  16431  djucllem  16501  012of  16696  2o01f  16697  nninfsellemeq  16723  qdencn  16738  cvgcmp2nlemabs  16747  trilpolemclim  16751  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  nconstwlpolemgt0  16780  gfsumval  16792  gfsumsn  16797  gfsumcl  16799