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 1397   ∈ 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  3635  ifcldcd  3643  intab  3957  disjiun  4083  iinexgm  4244  opexg  4320  tfisi  4685  nnpredcl  4721  opabssxpd  4762  imain  5412  fvmptd  5727  fvmptdf  5734  fvmptt  5738  elfvmptrab  5742  dffo3  5794  resfunexg  5874  f1oiso2  5967  riota2df  5992  riota5f  5997  ovmpodxf  6146  ovmpodf  6152  offval  6242  ofvalg  6244  offeq  6248  iunexg  6280  oprabexd  6288  fo1stresm  6323  fo2ndresm  6324  oprssdmm  6333  1stdm  6344  1stconst  6385  2ndconst  6386  cnvf1olem  6388  fo2ndf  6391  f1od2  6399  iunon  6449  tfrlemibacc  6491  tfrlemibfn  6493  tfr1onlembacc  6507  tfr1onlembfn  6509  tfrcllembacc  6520  tfrcllembfn  6522  tfrcl  6529  rdgon  6551  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  oacl  6627  omcl  6628  oeicl  6629  nntr2  6670  mptelixpg  6902  fidifsnen  7056  en2eqpr  7098  unfiin  7117  tpfidceq  7121  ssfirab  7128  fnfi  7134  relcnvfi  7139  fidcenumlemr  7153  elfi2  7170  supclti  7196  supubti  7197  suplubti  7198  supelti  7200  ordiso2  7233  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djuss  7268  updjudhcoinlf  7278  updjudhcoinrg  7279  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  nninfwlpoimlemg  7373  cardcl  7384  exmidontriimlem2  7436  exmidapne  7478  cc2lem  7484  cc3  7486  addclpi  7546  mulclpi  7547  addclnq  7594  mulclnq  7595  addclnq0  7670  mulclnq0  7671  nqpnq0nq  7672  elnp1st2nd  7695  prarloclemcalc  7721  distrlem1prl  7801  distrlem1pru  7802  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  addcanprlemu  7834  recexprlemloc  7850  aptiprleml  7858  caucvgprprlemopl  7916  suplocexprlemex  7941  addclsr  7972  mulclsr  7973  recexgt0sr  7992  mulextsr1lem  7999  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axaddcl  8083  axaddrcl  8084  axmulcl  8085  axmulrcl  8086  axcaucvglemval  8116  subcl  8377  cru  8781  aprcl  8825  aptap  8829  divclap  8857  redivclap  8910  diveqap1bd  9015  lbinfcl  9128  cju  9140  nn1m1nn  9160  nnsub  9181  nnnn0addcl  9431  un0addcl  9434  peano2z  9514  peano2zm  9516  zaddcllemneg  9517  zaddcl  9518  nnaddm1cl  9540  nn0n0n1ge2  9549  zdivadd  9568  zdivmul  9569  suprzclex  9577  zneo  9580  peano5uzti  9587  supinfneg  9828  infsupneg  9829  qmulz  9856  qnegcl  9869  qapne  9872  qdivcl  9876  cnref1o  9884  xnegcl  10066  xltnegi  10069  xaddnemnf  10091  xaddnepnf  10092  xnegdi  10102  xnpcan  10106  xltadd1  10110  xposdif  10116  xleaddadd  10121  iccf1o  10238  ige3m2fz  10283  ige2m1fz1  10343  zssinfcl  10491  infssuzex  10492  infssuzcldc  10494  zsupssdc  10497  suprzcl2dc  10498  rebtwn2z  10513  flqcl  10532  flapcl  10534  ceilqcl  10569  intfracq  10581  modqcl  10587  mulqmod0  10591  modqdifz  10597  zmodcl  10605  modfzo0difsn  10656  modsumfzodifsn  10657  frec2uzzd  10661  frec2uzsucd  10662  frec2uzuzd  10663  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgsuctlem  10684  fzofig  10693  iseqovex  10719  seq3val  10721  seqvalcd  10722  seqf  10725  seqovcd  10728  seq3clss  10732  seq3caopr3  10752  iseqf1olemnab  10762  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem2a  10779  seqf1oglem1  10780  seqf1oglem2  10781  seq3distr  10793  ser0f  10795  ser3le  10798  exp3vallem  10801  exp3val  10802  exp1  10806  expcl2lemap  10812  m1expcl2  10822  expaddzap  10844  sqcl  10861  nnsqcl  10870  qsqcl  10872  zesq  10919  facp1  10991  faccl  10996  facdiv  10999  bcval  11010  bcrpcl  11014  bcp1n  11022  bcpasc  11027  permnn  11032  hashennn  11041  hashcl  11042  lencl  11116  wrdexg  11123  elovmpowrd  11154  lswcl  11163  ccatcl  11169  ccatrn  11185  lswccatn0lsw  11187  ccatalpha  11189  s1cl  11197  swrdclg  11230  swrdwrdsymbg  11244  ccatswrd  11250  pfxval  11254  fnpfx  11257  pfxclg  11258  pfxwrdsymbg  11270  ccatpfx  11281  lenrevpfxcctswrd  11292  wrdind  11302  wrd2ind  11303  shftlem  11376  ovshftex  11379  shftf  11390  seq3shft  11398  cjth  11406  imval  11410  recl  11413  imcl  11414  crre  11417  remim  11420  reim0b  11422  cvg1nlemcau  11544  uzin2  11547  resqrexlem1arp  11565  resqrexlemp1rp  11566  resqrexlemglsq  11582  resqrexlemga  11583  resqrtcl  11589  abscl  11611  absrpclap  11621  nn0abscl  11645  fzomaxdiflem  11672  fzomaxdif  11673  maxabslemab  11766  maxcl  11770  zmaxcl  11784  minmax  11790  mincl  11791  xrmaxcl  11812  xrmaxaddlem  11820  xrminmax  11825  xrmincl  11826  xrmineqinf  11829  xrminrpcl  11834  reccn2ap  11873  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  climle  11894  climlec2  11901  climcvg1nlem  11909  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsumgcl  11946  fsum3  11947  isumss  11951  fisumss  11952  isumss2  11953  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumcllem  11959  fsumadd  11966  sumsnf  11969  fsumsplitsn  11970  isumcl  11985  isummulc2  11986  isumrecl  11989  isumge0  11990  isumadd  11991  fsum2dlemstep  11994  fisumcom2  11998  mptfzshft  12002  fsumrev  12003  fsummulc2  12008  iserabs  12035  isumshft  12050  isumsplit  12051  isum1p  12052  isumrpcl  12054  isumle  12055  isumlessdc  12056  trireciplem  12060  expcnvap0  12062  expcnvre  12063  expcnv  12064  explecnv  12065  geolim  12071  geolim2  12072  geo2lim  12076  cvgratnnlemsumlt  12088  cvgratz  12092  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodf1f  12103  prodfdivap  12107  prodrbdclem  12131  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prodssdc  12149  fprodmul  12151  prodsnf  12152  fprodsplitdc  12156  fprodunsn  12164  fprodcl2lem  12165  fprodcllem  12166  fprodabs  12176  fprodrev  12179  fprod2dlemstep  12182  fprodcom2fi  12186  fprodsplitsn  12193  efcllemp  12218  ef0lem  12220  efcvgfsum  12227  reefcl  12228  ege2le3  12231  efcj  12233  efaddlem  12234  eftlcvg  12247  eftlcl  12248  reeftlcl  12249  eftlub  12250  efsep  12251  effsumlt  12252  efgt1p2  12255  efgt1p  12256  reeff1  12260  tanclap  12269  resincl  12280  recoscl  12281  retanclap  12282  eirraplem  12337  dvdsval2  12350  fsumdvds  12402  sqoddm1div8z  12446  bitsinv1lem  12521  gcdval  12529  gcdn0cl  12532  gcddvds  12533  divgcdnnr  12546  uzwodc  12607  nn0seqcvgd  12612  ialgrlem1st  12613  ialgrlemconst  12614  algrf  12616  algrp1  12617  eucalgf  12626  eucalglt  12628  lcmval  12634  lcmcllem  12638  lcmgcdlem  12648  cncongr2  12675  sqrt2irrlem  12732  oddpwdclemxy  12740  oddpwdclemdc  12744  qden1elz  12776  phicl2  12785  phimullem  12796  eulerthlemth  12803  prmdiv  12806  odzcllem  12814  pythagtriplem8  12844  pythagtriplem9  12845  pcval  12868  pczcl  12870  pcqcl  12878  dvdsprmpweqle  12909  pcaddlem  12911  pcmptcl  12914  pcmpt  12915  pockthlem  12928  pockthg  12929  zgz  12945  gznegcl  12947  gzcjcl  12948  gzaddcl  12949  gzmulcl  12950  gzabssqcl  12953  4sqlem5  12954  4sqlem4a  12963  mul4sqlem  12965  mul4sq  12966  4sqlemafi  12967  4sqlemffi  12968  4sqleminfi  12969  4sqexercise1  12970  4sqlem16  12978  4sqlem17  12979  ennnfonelemjn  13022  ennnfonelemg  13023  ennnfonelemp1  13026  ctinfomlemom  13047  ctiunctlemfo  13059  nninfdclemcl  13068  nninfdclemf  13069  nninfdclemp1  13070  setsex  13113  strsetsid  13114  strslfv3  13127  bassetsnn  13138  ressex  13147  ressbas2d  13150  strressid  13153  tgvalex  13345  ptex  13346  prdsex  13351  prdsval  13355  imasex  13387  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfn  13399  imasaddval  13400  imasaddf  13401  imasmulfn  13402  imasmulval  13403  imasmulf  13404  qusval  13405  qusex  13407  qusaddvallemg  13415  qusaddflemg  13416  qusaddval  13417  qusaddf  13418  qusmulval  13419  qusmulf  13420  mgm1  13452  gsumress  13477  gsumprval  13481  prdsplusgsgrpcl  13496  prdsplusgcl  13528  prdsidlem  13529  pwsmnd  13532  mhmex  13544  subsubm  13565  0subm  13566  mhmeql  13574  gsumwsubmcl  13578  gsumfzcl  13581  grpsubval  13628  grplinv  13632  pwsgrp  13693  qusgrp2  13699  mulgval  13708  mulgex  13709  mulgfng  13710  mulg1  13715  mulgnnp1  13716  mulgnnsubcl  13720  mulgnn0subcl  13721  mulgsubcl  13722  mulgnndir  13737  subgex  13762  subgsubcl  13771  issubgrpd  13777  subsubg  13783  nsgconj  13792  0nsg  13800  triv1nsgd  13804  eqgex  13807  eqger  13810  eqgcpbl  13814  ghmex  13841  ghmpreima  13852  ghmnsgpreima  13855  conjnmz  13865  gsumfzsubmcl  13924  mgpex  13937  rngmgpf  13949  qusrng  13970  mgpf  14023  qusring2  14078  opprex  14085  opprrng  14089  opprring  14091  dvdsrex  14111  opprunitd  14123  dvrvald  14147  dvrcl  14148  unitdvcl  14149  invrpropdg  14162  subsubrng  14227  subrgcrng  14238  subrgsubm  14247  subrgugrp  14253  subsubrg  14258  rnrhmsubrg  14265  aprcotr  14298  rmodislmod  14364  lssvsubcl  14379  islss3  14392  lspex  14408  ellspsn  14430  sraex  14459  rlmlmod  14477  lidlex  14486  rspex  14487  lidl0cl  14496  lidlacl  14497  lidlnegcl  14498  ridl0  14523  ridl1  14524  2idlelbas  14529  cnsubglem  14592  expghmap  14620  mulgrhm  14622  zrhex  14634  znbaslemnn  14652  psrval  14679  psrbagfi  14686  psrbasg  14687  mplsubgfilemm  14711  mplsubgfilemcl  14712  mplsubgfileminv  14713  mplgrpfi  14719  iunopn  14725  toponmax  14748  tgtop  14791  tgiun  14796  tgidm  14797  ntropn  14840  tgrest  14892  restopnb  14904  cnovex  14919  cnclima  14946  txvalex  14977  txtop  14983  tx1cn  14992  tx2cn  14993  txcnp  14994  txcnmpt  14996  txdis1cn  15001  cnmptcom  15021  imasnopn  15022  hmeocnv  15030  hmeores  15038  txhmeo  15042  txswaphmeo  15044  ispsmet  15046  xmetres  15105  metres  15106  blex  15110  xmeter  15159  xmetresbl  15163  mopntopon  15166  isxms2  15175  xmetxp  15230  xmettx  15233  txmetcnp  15241  qtopbasss  15244  qtopbas  15245  reopnap  15269  ioo2blex  15275  blssioo  15276  tgioo  15277  fsumcncntop  15290  expcn  15292  cncfval  15295  divccncfap  15313  cdivcncfap  15327  divcncfap  15337  maxcncf  15338  mincncf  15339  ivthdec  15367  hoverb  15371  limccnpcntop  15398  dvrecap  15436  elplyd  15464  ply1termlem  15465  ply1term  15466  plymullem1  15471  plyaddlem  15472  plymullem  15473  plycolemc  15481  plyco  15482  plycj  15484  plycn  15485  plyreres  15487  dvply1  15488  dvply2g  15489  pilem3  15506  tanrpcl  15560  cosordlem  15572  ioocosf1o  15577  rpcncxpcl  15625  rpcxpcl  15626  rpabscxpbnd  15663  rplogbcl  15669  sgmnncl  15711  mpodvdsmulf1o  15713  fsumdvdsmul  15714  mersenne  15720  perfectlem2  15723  lgslem1  15728  lgsval  15732  lgscllem  15735  lgsne0  15766  gausslemma2dlem4  15792  lgseisenlem1  15798  lgsquadlem1  15805  lgsquadlem2  15806  2sqlem3  15845  2sqlem8  15851  vtxex  15868  iedgex  15869  edgvalg  15909  edgopval  15912  edgstruct  15914  usgrausgrien  16019  ausgrumgrien  16020  ausgrusgrien  16021  uspgr1ewopdc  16094  usgr2v1e2w  16096  uhgrspansubgrlem  16126  vtxdgfif  16143  vtxdfifiun  16147  1loopgrvd2fi  16155  1loopgrvd0fi  16156  1hevtxdg0fi  16157  1hevtxdg1en  16158  p1evtxdeqfilem  16161  vdegp1bid  16165  wlkex  16175  wlkelvv  16199  clwwlkccat  16251  clwwlknonex2lem1  16287  clwwlknonex2lem2  16288  clwwlknonex2  16289  trlsegvdeglem6  16315  trlsegvdeglem7  16316  djucllem  16396  012of  16592  2o01f  16593  nninfsellemeq  16616  qdencn  16631  cvgcmp2nlemabs  16636  trilpolemclim  16640  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  nconstwlpolemgt0  16668  gfsumval  16680