Theorem eqeltrd 2315

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eqeltrrd  2316  3eltr4d  2322  eqeltrid  2325  eqeltrdi  2329  ifcldadc  3667  ifcldcd  3675  intab  3994  disjiun  4120  iinexgm  4285  opexg  4363  tfisi  4729  nnpredcl  4765  opabssxpd  4806  imain  5458  fvmptd  5780  fvmptdf  5787  fvmptt  5791  elfvmptrab  5795  dffo3  5846  resfunexg  5927  f1oiso2  6023  riota2df  6050  riota5f  6055  ovmpodxf  6204  ovmpodf  6210  offval  6300  ofvalg  6302  offeq  6306  iunexg  6338  oprabexd  6350  fo1stresm  6385  fo2ndresm  6386  oprssdmm  6395  1stdm  6406  1stconst  6447  2ndconst  6448  cnvf1olem  6450  fo2ndf  6453  f1od2  6461  iunon  6545  tfrlemibacc  6587  tfrlemibfn  6589  tfr1onlembacc  6603  tfr1onlembfn  6605  tfrcllembacc  6616  tfrcllembfn  6618  tfrcl  6625  rdgon  6647  frec0g  6658  freccllem  6663  frecfcllem  6665  frecsuclem  6667  oacl  6723  omcl  6724  oeicl  6725  nntr2  6766  mptelixpg  7006  fidifsnen  7162  en2eqpr  7204  unfiin  7223  tpfidceq  7227  ssfirab  7234  fnfi  7240  relcnvfi  7245  fidcenumlemr  7262  snopfsuppdc  7289  fsuppcorn  7291  elfi2  7296  supclti  7328  supubti  7329  suplubti  7330  supelti  7332  ordiso2  7365  djulclr  7379  djurclr  7380  djulcl  7381  djurcl  7382  djuss  7400  updjudhcoinlf  7410  updjudhcoinrg  7411  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  nninfwlpoimlemg  7505  cardcl  7516  exmidontriimlem2  7568  exmidapne  7616  cc2lem  7622  cc3  7624  addclpi  7684  mulclpi  7685  addclnq  7732  mulclnq  7733  addclnq0  7808  mulclnq0  7809  nqpnq0nq  7810  elnp1st2nd  7833  prarloclemcalc  7859  distrlem1prl  7939  distrlem1pru  7940  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  addcanprlemu  7972  recexprlemloc  7988  aptiprleml  7996  caucvgprprlemopl  8054  suplocexprlemex  8079  addclsr  8110  mulclsr  8111  recexgt0sr  8130  mulextsr1lem  8137  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axaddcl  8221  axaddrcl  8222  axmulcl  8223  axmulrcl  8224  axcaucvglemval  8254  subcl  8515  cru  8920  aprcl  8964  aptap  8968  divclap  8998  redivclap  9051  diveqap1bd  9156  lbinfcl  9269  cju  9281  nn1m1nn  9301  nnsub  9322  nnnn0addcl  9572  un0addcl  9575  peano2z  9659  peano2zm  9661  zaddcllemneg  9662  zaddcl  9663  nnaddm1cl  9685  nn0n0n1ge2  9694  zdivadd  9714  zdivmul  9715  suprzclex  9723  zneo  9726  peano5uzti  9733  supinfneg  9974  infsupneg  9975  qmulz  10002  qnegcl  10015  qapne  10018  qdivcl  10022  cnref1o  10030  xnegcl  10213  xltnegi  10216  xaddnemnf  10238  xaddnepnf  10239  xnegdi  10249  xnpcan  10253  xltadd1  10257  xposdif  10263  xleaddadd  10268  iccf1o  10386  ige3m2fz  10432  ige2m1fz1  10494  zssinfcl  10643  infssuzex  10644  infssuzcldc  10646  zsupssdc  10651  suprzcl2dc  10652  rebtwn2z  10667  flqcl  10686  flapcl  10688  ceilqcl  10723  intfracq  10735  modqcl  10741  mulqmod0  10745  modqdifz  10751  zmodcl  10759  modfzo0difsn  10810  modsumfzodifsn  10811  frec2uzzd  10815  frec2uzsucd  10816  frec2uzuzd  10817  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgsuctlem  10838  fzofig  10847  iseqovex  10873  seq3val  10875  seqvalcd  10876  seqf  10879  seqovcd  10882  seq3clss  10886  seq3caopr3  10906  iseqf1olemnab  10916  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsum  10928  seq3f1oleml  10931  seq3f1o  10932  seqf1oglem2a  10933  seqf1oglem1  10934  seqf1oglem2  10935  seq3distr  10947  ser0f  10949  ser3le  10952  exp3vallem  10955  exp3val  10956  exp1  10960  expcl2lemap  10966  m1expcl2  10976  expaddzap  10998  sqcl  11015  nnsqcl  11024  qsqcl  11026  zesq  11074  facp1  11146  faccl  11151  facdiv  11154  bcval  11165  bcrpcl  11169  bcp1n  11177  bcpasc  11182  permnn  11188  hashennn  11197  hashcl  11198  hashf1  11265  lencl  11286  wrdexg  11293  elovmpowrd  11324  lswcl  11333  ccatcl  11339  ccatrn  11355  lswccatn0lsw  11357  ccatalpha  11359  s1cl  11367  swrdclg  11400  swrdwrdsymbg  11414  ccatswrd  11420  pfxval  11424  fnpfx  11427  pfxclg  11428  pfxwrdsymbg  11440  ccatpfx  11451  lenrevpfxcctswrd  11462  wrdind  11472  wrd2ind  11473  shftlem  11559  ovshftex  11562  shftf  11573  seq3shft  11581  cjth  11589  imval  11593  recl  11596  imcl  11597  crre  11600  remim  11603  reim0b  11605  cvg1nlemcau  11728  uzin2  11731  resqrexlem1arp  11749  resqrexlemp1rp  11750  resqrexlemglsq  11766  resqrexlemga  11767  resqrtcl  11773  abscl  11795  absrpclap  11805  nn0abscl  11829  fzomaxdiflem  11856  fzomaxdif  11857  maxabslemab  11950  maxcl  11954  zmaxcl  11968  minmax  11974  mincl  11975  xrmaxcl  11996  xrmaxaddlem  12004  xrminmax  12009  xrmincl  12010  xrmineqinf  12013  xrminrpcl  12018  reccn2ap  12057  climaddc1  12073  climmulc2  12075  climsubc1  12076  climsubc2  12077  climle  12078  climlec2  12085  climcvg1nlem  12093  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsumgcl  12131  fsum3  12132  isumss  12136  fisumss  12137  isumss2  12138  fsum3cvg2  12139  fsum3ser  12142  fsumcl2lem  12143  fsumcllem  12144  fsumadd  12151  sumsnf  12154  fsumsplitsn  12155  isumcl  12170  isummulc2  12171  isumrecl  12174  isumge0  12175  isumadd  12176  fsum2dlemstep  12179  fisumcom2  12183  mptfzshft  12187  fsumrev  12188  fsummulc2  12193  iserabs  12220  isumshft  12235  isumsplit  12236  isum1p  12237  isumrpcl  12239  isumle  12240  isumlessdc  12241  trireciplem  12245  expcnvap0  12247  expcnvre  12248  expcnv  12249  explecnv  12250  geolim  12256  geolim2  12257  geo2lim  12261  cvgratnnlemsumlt  12273  cvgratz  12277  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodf1f  12288  prodfdivap  12292  prodrbdclem  12316  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prodssdc  12334  fprodmul  12336  prodsnf  12337  fprodsplitdc  12341  fprodunsn  12349  fprodcl2lem  12350  fprodcllem  12351  fprodabs  12361  fprodrev  12364  fprod2dlemstep  12367  fprodcom2fi  12371  fprodsplitsn  12378  efcllemp  12403  ef0lem  12405  efcvgfsum  12412  reefcl  12413  ege2le3  12416  efcj  12418  efaddlem  12419  eftlcvg  12432  eftlcl  12433  reeftlcl  12434  eftlub  12435  efsep  12436  effsumlt  12437  efgt1p2  12440  efgt1p  12441  reeff1  12445  tanclap  12454  resincl  12465  recoscl  12466  retanclap  12467  eirraplem  12522  dvdsval2  12535  fsumdvds  12587  sqoddm1div8z  12631  bitsinv1lem  12706  gcdval  12714  gcdn0cl  12717  gcddvds  12718  divgcdnnr  12731  uzwodc  12792  nn0seqcvgd  12797  ialgrlem1st  12798  ialgrlemconst  12799  algrf  12801  algrp1  12802  eucalgf  12811  eucalglt  12813  lcmval  12819  lcmcllem  12823  lcmgcdlem  12833  cncongr2  12860  sqrt2irrlem  12917  oddpwdclemxy  12925  oddpwdclemdc  12929  qden1elz  12961  phicl2  12970  phimullem  12981  eulerthlemth  12988  prmdiv  12991  odzcllem  12999  pythagtriplem8  13029  pythagtriplem9  13030  pcval  13053  pczcl  13055  pcqcl  13063  dvdsprmpweqle  13094  pcaddlem  13096  pcmptcl  13099  pcmpt  13100  pockthlem  13113  pockthg  13114  zgz  13130  gznegcl  13132  gzcjcl  13133  gzaddcl  13134  gzmulcl  13135  gzabssqcl  13138  4sqlem5  13139  4sqlem4a  13148  mul4sqlem  13150  mul4sq  13151  4sqlemafi  13152  4sqlemffi  13153  4sqleminfi  13154  4sqexercise1  13155  4sqlem16  13163  4sqlem17  13164  ballotfilemfelz  13208  ballotfilemiex  13222  ballotfilemsdom  13233  ballotfilemgval  13245  ennnfonelemjn  13271  ennnfonelemg  13272  ennnfonelemp1  13275  ctinfomlemom  13296  ctiunctlemfo  13308  nninfdclemcl  13317  nninfdclemf  13318  nninfdclemp1  13319  setsex  13362  strsetsid  13363  strslfv3  13376  bassetsnn  13387  ressex  13396  ressbas2d  13399  strressid  13402  tgvalex  13594  ptex  13595  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfn  13615  imasaddval  13616  imasaddf  13617  imasmulfn  13618  imasmulval  13619  imasmulf  13620  qusval  13621  qusex  13623  qusaddvallemg  13631  qusaddflemg  13632  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  mgm1  13667  gzsumress  13689  mhmex  13746  subsubm  13767  0subm  13768  mhmeql  13776  gzsumwsubmcl  13778  gzsumcl  13781  grpsubval  13828  grplinv  13832  qusgrp2  13893  mulgval  13902  mulgex  13903  mulgfng  13904  mulg1  13909  mulgnnp1  13910  mulgnnsubcl  13914  mulgnn0subcl  13915  mulgsubcl  13916  mulgnndir  13931  subgex  13956  subgsubcl  13965  issubgrpd  13971  subsubg  13977  nsgconj  13986  0nsg  13994  triv1nsgd  13998  eqgex  14001  eqger  14004  eqgcpbl  14008  ghmex  14035  ghmpreima  14046  ghmnsgpreima  14049  conjnmz  14059  gzsumsubmcl  14119  gzsumsplit0  14125  gsumvalfi  14129  gsumsncmn  14133  gsumclfi  14136  gsumsubmclfi  14140  prdsex  14149  prdsval  14150  prdsplusgsgrpcl  14167  prdsplusgcl  14169  prdsidlem  14170  pwsmnd  14189  pwsgrp  14191  mgpex  14199  rngmgpf  14211  qusrng  14232  mgpf  14289  qusring2  14344  opprex  14351  opprrng  14355  opprring  14357  dvdsrex  14378  opprunitd  14390  dvrvald  14414  dvrcl  14415  unitdvcl  14416  invrpropdg  14429  subsubrng  14495  subrgcrng  14506  subrgsubm  14515  subrgugrp  14521  subsubrg  14526  rnrhmsubrg  14533  aprcotr  14570  aprnzr  14572  aprlring  14573  rmodislmod  14660  lssvsubcl  14675  islss3  14688  lspex  14704  ellspsn  14726  sraex  14755  rlmlmod  14773  lidlex  14782  rspex  14783  lidl0cl  14792  lidlacl  14793  lidlnegcl  14794  ridl0  14819  ridl1  14820  2idlelbas  14825  cnsubglem  14888  expghmap  14914  mulgrhm  14916  zrhex  14928  znbaslemnn  14946  psrval  14973  psrbagfi  14982  psrbagcon  14985  psrbasg  14988  mplsubgfilemm  15012  mplsubgfilemcl  15013  mplsubgfileminv  15014  mplgrpfi  15020  iunopn  15026  toponmax  15049  tgtop  15092  tgiun  15097  tgidm  15098  ntropn  15141  tgrest  15193  restopnb  15205  cnovex  15220  cnclima  15247  txvalex  15278  txtop  15284  tx1cn  15293  tx2cn  15294  txcnp  15295  txcnmpt  15297  txdis1cn  15302  cnmptcom  15322  imasnopn  15323  hmeocnv  15331  hmeores  15339  txhmeo  15343  txswaphmeo  15345  ispsmet  15347  xmetres  15406  metres  15407  blex  15411  xmeter  15460  xmetresbl  15464  mopntopon  15467  isxms2  15476  xmetxp  15531  xmettx  15534  txmetcnp  15542  qtopbasss  15545  qtopbas  15546  reopnap  15570  ioo2blex  15576  blssioo  15577  tgioo  15578  fsumcncntop  15591  expcn  15593  cncfval  15596  divccncfap  15614  cdivcncfap  15628  divcncfap  15638  maxcncf  15639  mincncf  15640  ivthdec  15668  hoverb  15672  limccnpcntop  15699  dvrecap  15737  elplyd  15765  ply1termlem  15766  ply1term  15767  plymullem1  15772  plyaddlem  15773  plymullem  15774  plycolemc  15782  plyco  15783  plycj  15785  plycn  15786  plyreres  15788  dvply1  15789  dvply2g  15790  pilem3  15807  tanrpcl  15861  cosordlem  15873  ioocosf1o  15878  logfac  15918  rpcncxpcl  15927  rpcxpcl  15928  rpabscxpbnd  15965  rplogbcl  15971  pellexlem1  16005  sgmnncl  16016  mpodvdsmulf1o  16018  fsumdvdsmul  16019  mersenne  16025  perfectlem2  16028  lgslem1  16033  lgsval  16037  lgscllem  16040  lgsne0  16071  gausslemma2dlem4  16097  lgseisenlem1  16103  lgsquadlem1  16110  lgsquadlem2  16111  2sqlem3  16150  2sqlem8  16156  vtxex  16173  iedgex  16174  edgvalg  16214  edgopval  16217  edgstruct  16219  usgrausgrien  16324  ausgrumgrien  16325  ausgrusgrien  16326  uspgr1ewopdc  16399  usgr2v1e2w  16401  uhgrspansubgrlem  16431  vtxdgfif  16448  vtxdfifiun  16452  1loopgrvd2fi  16460  1loopgrvd0fi  16461  1hevtxdg0fi  16462  1hevtxdg1en  16463  p1evtxdeqfilem  16466  vdegp1bid  16470  wlkex  16480  wlkelvv  16504  clwwlkccat  16556  clwwlknonex2lem1  16592  clwwlknonex2lem2  16593  clwwlknonex2  16594  trlsegvdeglem6  16620  trlsegvdeglem7  16621  trlsegvdegfi  16622  eupth2lem3lem1fi  16623  eupth2lem3lem2fi  16624  eupth2lem3lem5  16627  eupth2lembfi  16632  eulerpathprum  16635  depindlem1  16661  depindlem2  16662  djucllem  16742  012of  16937  2o01f  16938  nninfsellemeq  16962  qdencn  16977  cvgcmp2nlemabs  16986  trilpolemclim  16990  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  nconstwlpolemgt0  17019