Theorem eqeltrd 2284

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eqeltrrd  2285  3eltr4d  2291  eqeltrid  2294  eqeltrdi  2298  ifcldadc  3609  ifcldcd  3617  intab  3928  disjiun  4054  iinexgm  4214  opexg  4290  tfisi  4653  nnpredcl  4689  imain  5375  fvmptd  5683  fvmptdf  5690  fvmptt  5694  elfvmptrab  5698  dffo3  5750  resfunexg  5828  f1oiso2  5919  riota2df  5943  riota5f  5947  ovmpodxf  6094  ovmpodf  6100  offval  6189  ofvalg  6191  offeq  6195  iunexg  6227  oprabexd  6235  fo1stresm  6270  fo2ndresm  6271  oprssdmm  6280  1stdm  6291  1stconst  6330  2ndconst  6331  cnvf1olem  6333  fo2ndf  6336  f1od2  6344  iunon  6393  tfrlemibacc  6435  tfrlemibfn  6437  tfr1onlembacc  6451  tfr1onlembfn  6453  tfrcllembacc  6464  tfrcllembfn  6466  tfrcl  6473  rdgon  6495  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  oacl  6569  omcl  6570  oeicl  6571  nntr2  6612  mptelixpg  6844  fidifsnen  6993  en2eqpr  7030  unfiin  7049  tpfidceq  7053  ssfirab  7059  fnfi  7064  relcnvfi  7069  fidcenumlemr  7083  elfi2  7100  supclti  7126  supubti  7127  suplubti  7128  supelti  7130  ordiso2  7163  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  djuss  7198  updjudhcoinlf  7208  updjudhcoinrg  7209  ctssdclemn0  7238  ctssdccl  7239  ctssdc  7241  enumctlemm  7242  nninfwlpoimlemg  7303  cardcl  7314  exmidontriimlem2  7365  exmidapne  7407  cc2lem  7413  cc3  7415  addclpi  7475  mulclpi  7476  addclnq  7523  mulclnq  7524  addclnq0  7599  mulclnq0  7600  nqpnq0nq  7601  elnp1st2nd  7624  prarloclemcalc  7650  distrlem1prl  7730  distrlem1pru  7731  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  addcanprlemu  7763  recexprlemloc  7779  aptiprleml  7787  caucvgprprlemopl  7845  suplocexprlemex  7870  addclsr  7901  mulclsr  7902  recexgt0sr  7921  mulextsr1lem  7928  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axaddcl  8012  axaddrcl  8013  axmulcl  8014  axmulrcl  8015  axcaucvglemval  8045  subcl  8306  cru  8710  aprcl  8754  aptap  8758  divclap  8786  redivclap  8839  diveqap1bd  8944  lbinfcl  9057  cju  9069  nn1m1nn  9089  nnsub  9110  nnnn0addcl  9360  un0addcl  9363  peano2z  9443  peano2zm  9445  zaddcllemneg  9446  zaddcl  9447  nnaddm1cl  9469  nn0n0n1ge2  9478  zdivadd  9497  zdivmul  9498  suprzclex  9506  zneo  9509  peano5uzti  9516  supinfneg  9751  infsupneg  9752  qmulz  9779  qnegcl  9792  qapne  9795  qdivcl  9799  cnref1o  9807  xnegcl  9989  xltnegi  9992  xaddnemnf  10014  xaddnepnf  10015  xnegdi  10025  xnpcan  10029  xltadd1  10033  xposdif  10039  xleaddadd  10044  iccf1o  10161  ige3m2fz  10206  ige2m1fz1  10266  zssinfcl  10412  infssuzex  10413  infssuzcldc  10415  zsupssdc  10418  suprzcl2dc  10419  rebtwn2z  10434  flqcl  10453  flapcl  10455  ceilqcl  10490  intfracq  10502  modqcl  10508  mulqmod0  10512  modqdifz  10518  zmodcl  10526  modfzo0difsn  10577  modsumfzodifsn  10578  frec2uzzd  10582  frec2uzsucd  10583  frec2uzuzd  10584  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgsuctlem  10605  fzofig  10614  iseqovex  10640  seq3val  10642  seqvalcd  10643  seqf  10646  seqovcd  10649  seq3clss  10653  seq3caopr3  10673  iseqf1olemnab  10683  iseqf1olemqk  10689  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsumkj  10693  seq3f1olemqsum  10695  seq3f1oleml  10698  seq3f1o  10699  seqf1oglem2a  10700  seqf1oglem1  10701  seqf1oglem2  10702  seq3distr  10714  ser0f  10716  ser3le  10719  exp3vallem  10722  exp3val  10723  exp1  10727  expcl2lemap  10733  m1expcl2  10743  expaddzap  10765  sqcl  10782  nnsqcl  10791  qsqcl  10793  zesq  10840  facp1  10912  faccl  10917  facdiv  10920  bcval  10931  bcrpcl  10935  bcp1n  10943  bcpasc  10948  permnn  10953  hashennn  10962  hashcl  10963  lencl  11035  wrdexg  11042  elovmpowrd  11072  lswcl  11081  ccatcl  11087  ccatrn  11103  lswccatn0lsw  11105  s1cl  11113  swrdclg  11141  swrdwrdsymbg  11155  ccatswrd  11161  pfxval  11165  fnpfx  11168  pfxclg  11169  pfxwrdsymbg  11181  ccatpfx  11192  lenrevpfxcctswrd  11203  wrdind  11213  wrd2ind  11214  shftlem  11242  ovshftex  11245  shftf  11256  seq3shft  11264  cjth  11272  imval  11276  recl  11279  imcl  11280  crre  11283  remim  11286  reim0b  11288  cvg1nlemcau  11410  uzin2  11413  resqrexlem1arp  11431  resqrexlemp1rp  11432  resqrexlemglsq  11448  resqrexlemga  11449  resqrtcl  11455  abscl  11477  absrpclap  11487  nn0abscl  11511  fzomaxdiflem  11538  fzomaxdif  11539  maxabslemab  11632  maxcl  11636  zmaxcl  11650  minmax  11656  mincl  11657  xrmaxcl  11678  xrmaxaddlem  11686  xrminmax  11691  xrmincl  11692  xrmineqinf  11695  xrminrpcl  11700  reccn2ap  11739  climaddc1  11755  climmulc2  11757  climsubc1  11758  climsubc2  11759  climle  11760  climlec2  11767  climcvg1nlem  11775  sumrbdclem  11803  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  zsumdc  11810  fsumgcl  11812  fsum3  11813  isumss  11817  fisumss  11818  isumss2  11819  fsum3cvg2  11820  fsum3ser  11823  fsumcl2lem  11824  fsumcllem  11825  fsumadd  11832  sumsnf  11835  fsumsplitsn  11836  isumcl  11851  isummulc2  11852  isumrecl  11855  isumge0  11856  isumadd  11857  fsum2dlemstep  11860  fisumcom2  11864  mptfzshft  11868  fsumrev  11869  fsummulc2  11874  iserabs  11901  isumshft  11916  isumsplit  11917  isum1p  11918  isumrpcl  11920  isumle  11921  isumlessdc  11922  trireciplem  11926  expcnvap0  11928  expcnvre  11929  expcnv  11930  explecnv  11931  geolim  11937  geolim2  11938  geo2lim  11942  cvgratnnlemsumlt  11954  cvgratz  11958  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodf1f  11969  prodfdivap  11973  prodrbdclem  11997  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prodssdc  12015  fprodmul  12017  prodsnf  12018  fprodsplitdc  12022  fprodunsn  12030  fprodcl2lem  12031  fprodcllem  12032  fprodabs  12042  fprodrev  12045  fprod2dlemstep  12048  fprodcom2fi  12052  fprodsplitsn  12059  efcllemp  12084  ef0lem  12086  efcvgfsum  12093  reefcl  12094  ege2le3  12097  efcj  12099  efaddlem  12100  eftlcvg  12113  eftlcl  12114  reeftlcl  12115  eftlub  12116  efsep  12117  effsumlt  12118  efgt1p2  12121  efgt1p  12122  reeff1  12126  tanclap  12135  resincl  12146  recoscl  12147  retanclap  12148  eirraplem  12203  dvdsval2  12216  fsumdvds  12268  sqoddm1div8z  12312  bitsinv1lem  12387  gcdval  12395  gcdn0cl  12398  gcddvds  12399  divgcdnnr  12412  uzwodc  12473  nn0seqcvgd  12478  ialgrlem1st  12479  ialgrlemconst  12480  algrf  12482  algrp1  12483  eucalgf  12492  eucalglt  12494  lcmval  12500  lcmcllem  12504  lcmgcdlem  12514  cncongr2  12541  sqrt2irrlem  12598  oddpwdclemxy  12606  oddpwdclemdc  12610  qden1elz  12642  phicl2  12651  phimullem  12662  eulerthlemth  12669  prmdiv  12672  odzcllem  12680  pythagtriplem8  12710  pythagtriplem9  12711  pcval  12734  pczcl  12736  pcqcl  12744  dvdsprmpweqle  12775  pcaddlem  12777  pcmptcl  12780  pcmpt  12781  pockthlem  12794  pockthg  12795  zgz  12811  gznegcl  12813  gzcjcl  12814  gzaddcl  12815  gzmulcl  12816  gzabssqcl  12819  4sqlem5  12820  4sqlem4a  12829  mul4sqlem  12831  mul4sq  12832  4sqlemafi  12833  4sqlemffi  12834  4sqleminfi  12835  4sqexercise1  12836  4sqlem16  12844  4sqlem17  12845  ennnfonelemjn  12888  ennnfonelemg  12889  ennnfonelemp1  12892  ctinfomlemom  12913  ctiunctlemfo  12925  nninfdclemcl  12934  nninfdclemf  12935  nninfdclemp1  12936  setsex  12979  strsetsid  12980  strslfv3  12993  ressex  13012  ressbas2d  13015  strressid  13018  tgvalex  13210  ptex  13211  prdsex  13216  prdsval  13220  imasex  13252  imasival  13253  imasbas  13254  imasplusg  13255  imasmulr  13256  imasaddfn  13264  imasaddval  13265  imasaddf  13266  imasmulfn  13267  imasmulval  13268  imasmulf  13269  qusval  13270  qusex  13272  qusaddvallemg  13280  qusaddflemg  13281  qusaddval  13282  qusaddf  13283  qusmulval  13284  qusmulf  13285  mgm1  13317  gsumress  13342  gsumprval  13346  prdsplusgsgrpcl  13361  prdsplusgcl  13393  prdsidlem  13394  pwsmnd  13397  mhmex  13409  subsubm  13430  0subm  13431  mhmeql  13439  gsumwsubmcl  13443  gsumfzcl  13446  grpsubval  13493  grplinv  13497  pwsgrp  13558  qusgrp2  13564  mulgval  13573  mulgex  13574  mulgfng  13575  mulg1  13580  mulgnnp1  13581  mulgnnsubcl  13585  mulgnn0subcl  13586  mulgsubcl  13587  mulgnndir  13602  subgex  13627  subgsubcl  13636  issubgrpd  13642  subsubg  13648  nsgconj  13657  0nsg  13665  triv1nsgd  13669  eqgex  13672  eqger  13675  eqgcpbl  13679  ghmex  13706  ghmpreima  13717  ghmnsgpreima  13720  conjnmz  13730  gsumfzsubmcl  13789  mgpex  13802  rngmgpf  13814  qusrng  13835  mgpf  13888  qusring2  13943  opprex  13950  opprrng  13954  opprring  13956  dvdsrex  13975  opprunitd  13987  dvrvald  14011  dvrcl  14012  unitdvcl  14013  invrpropdg  14026  subsubrng  14091  subrgcrng  14102  subrgsubm  14111  subrgugrp  14117  subsubrg  14122  rnrhmsubrg  14129  aprcotr  14162  rmodislmod  14228  lssvsubcl  14243  islss3  14256  lspex  14272  ellspsn  14294  sraex  14323  rlmlmod  14341  lidlex  14350  rspex  14351  lidl0cl  14360  lidlacl  14361  lidlnegcl  14362  ridl0  14387  ridl1  14388  2idlelbas  14393  cnsubglem  14456  expghmap  14484  mulgrhm  14486  zrhex  14498  znbaslemnn  14516  psrval  14543  psrbagfi  14550  psrbasg  14551  mplsubgfilemm  14575  mplsubgfilemcl  14576  mplsubgfileminv  14577  mplgrpfi  14583  iunopn  14589  toponmax  14612  tgtop  14655  tgiun  14660  tgidm  14661  ntropn  14704  tgrest  14756  restopnb  14768  cnovex  14783  cnclima  14810  txvalex  14841  txtop  14847  tx1cn  14856  tx2cn  14857  txcnp  14858  txcnmpt  14860  txdis1cn  14865  cnmptcom  14885  imasnopn  14886  hmeocnv  14894  hmeores  14902  txhmeo  14906  txswaphmeo  14908  ispsmet  14910  xmetres  14969  metres  14970  blex  14974  xmeter  15023  xmetresbl  15027  mopntopon  15030  isxms2  15039  xmetxp  15094  xmettx  15097  txmetcnp  15105  qtopbasss  15108  qtopbas  15109  reopnap  15133  ioo2blex  15139  blssioo  15140  tgioo  15141  fsumcncntop  15154  expcn  15156  cncfval  15159  divccncfap  15177  cdivcncfap  15191  divcncfap  15201  maxcncf  15202  mincncf  15203  ivthdec  15231  hoverb  15235  limccnpcntop  15262  dvrecap  15300  elplyd  15328  ply1termlem  15329  ply1term  15330  plymullem1  15335  plyaddlem  15336  plymullem  15337  plycolemc  15345  plyco  15346  plycj  15348  plycn  15349  plyreres  15351  dvply1  15352  dvply2g  15353  pilem3  15370  tanrpcl  15424  cosordlem  15436  ioocosf1o  15441  rpcncxpcl  15489  rpcxpcl  15490  rpabscxpbnd  15527  rplogbcl  15533  sgmnncl  15575  mpodvdsmulf1o  15577  fsumdvdsmul  15578  mersenne  15584  perfectlem2  15587  lgslem1  15592  lgsval  15596  lgscllem  15599  lgsne0  15630  gausslemma2dlem4  15656  lgseisenlem1  15662  lgsquadlem1  15669  lgsquadlem2  15670  2sqlem3  15709  2sqlem8  15715  vtxex  15732  iedgex  15733  edgvalg  15771  edgopval  15773  edgstruct  15775  djucllem  15936  012of  16130  2o01f  16131  nninfsellemeq  16153  qdencn  16168  cvgcmp2nlemabs  16173  trilpolemclim  16177  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  nconstwlpolemgt0  16205