Theorem eqeltrd 2306

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrd  2307  3eltr4d  2313  eqeltrid  2316  eqeltrdi  2320  ifcldadc  3632  ifcldcd  3640  intab  3952  disjiun  4078  iinexgm  4239  opexg  4315  tfisi  4680  nnpredcl  4716  opabssxpd  4757  imain  5406  fvmptd  5720  fvmptdf  5727  fvmptt  5731  elfvmptrab  5735  dffo3  5787  resfunexg  5867  f1oiso2  5960  riota2df  5985  riota5f  5990  ovmpodxf  6139  ovmpodf  6145  offval  6235  ofvalg  6237  offeq  6241  iunexg  6273  oprabexd  6281  fo1stresm  6316  fo2ndresm  6317  oprssdmm  6326  1stdm  6337  1stconst  6378  2ndconst  6379  cnvf1olem  6381  fo2ndf  6384  f1od2  6392  iunon  6441  tfrlemibacc  6483  tfrlemibfn  6485  tfr1onlembacc  6499  tfr1onlembfn  6501  tfrcllembacc  6512  tfrcllembfn  6514  tfrcl  6521  rdgon  6543  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  oacl  6619  omcl  6620  oeicl  6621  nntr2  6662  mptelixpg  6894  fidifsnen  7045  en2eqpr  7085  unfiin  7104  tpfidceq  7108  ssfirab  7114  fnfi  7119  relcnvfi  7124  fidcenumlemr  7138  elfi2  7155  supclti  7181  supubti  7182  suplubti  7183  supelti  7185  ordiso2  7218  djulclr  7232  djurclr  7233  djulcl  7234  djurcl  7235  djuss  7253  updjudhcoinlf  7263  updjudhcoinrg  7264  ctssdclemn0  7293  ctssdccl  7294  ctssdc  7296  enumctlemm  7297  nninfwlpoimlemg  7358  cardcl  7369  exmidontriimlem2  7420  exmidapne  7462  cc2lem  7468  cc3  7470  addclpi  7530  mulclpi  7531  addclnq  7578  mulclnq  7579  addclnq0  7654  mulclnq0  7655  nqpnq0nq  7656  elnp1st2nd  7679  prarloclemcalc  7705  distrlem1prl  7785  distrlem1pru  7786  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  addcanprlemu  7818  recexprlemloc  7834  aptiprleml  7842  caucvgprprlemopl  7900  suplocexprlemex  7925  addclsr  7956  mulclsr  7957  recexgt0sr  7976  mulextsr1lem  7983  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  axaddcl  8067  axaddrcl  8068  axmulcl  8069  axmulrcl  8070  axcaucvglemval  8100  subcl  8361  cru  8765  aprcl  8809  aptap  8813  divclap  8841  redivclap  8894  diveqap1bd  8999  lbinfcl  9112  cju  9124  nn1m1nn  9144  nnsub  9165  nnnn0addcl  9415  un0addcl  9418  peano2z  9498  peano2zm  9500  zaddcllemneg  9501  zaddcl  9502  nnaddm1cl  9524  nn0n0n1ge2  9533  zdivadd  9552  zdivmul  9553  suprzclex  9561  zneo  9564  peano5uzti  9571  supinfneg  9807  infsupneg  9808  qmulz  9835  qnegcl  9848  qapne  9851  qdivcl  9855  cnref1o  9863  xnegcl  10045  xltnegi  10048  xaddnemnf  10070  xaddnepnf  10071  xnegdi  10081  xnpcan  10085  xltadd1  10089  xposdif  10095  xleaddadd  10100  iccf1o  10217  ige3m2fz  10262  ige2m1fz1  10322  zssinfcl  10469  infssuzex  10470  infssuzcldc  10472  zsupssdc  10475  suprzcl2dc  10476  rebtwn2z  10491  flqcl  10510  flapcl  10512  ceilqcl  10547  intfracq  10559  modqcl  10565  mulqmod0  10569  modqdifz  10575  zmodcl  10583  modfzo0difsn  10634  modsumfzodifsn  10635  frec2uzzd  10639  frec2uzsucd  10640  frec2uzuzd  10641  frecuzrdgrrn  10647  frec2uzrdg  10648  frecuzrdgrcl  10649  frecuzrdgsuc  10653  frecuzrdgrclt  10654  frecuzrdgg  10655  frecuzrdgsuctlem  10662  fzofig  10671  iseqovex  10697  seq3val  10699  seqvalcd  10700  seqf  10703  seqovcd  10706  seq3clss  10710  seq3caopr3  10730  iseqf1olemnab  10740  iseqf1olemqk  10746  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  iseqf1olemfvp  10749  seq3f1olemqsumkj  10750  seq3f1olemqsum  10752  seq3f1oleml  10755  seq3f1o  10756  seqf1oglem2a  10757  seqf1oglem1  10758  seqf1oglem2  10759  seq3distr  10771  ser0f  10773  ser3le  10776  exp3vallem  10779  exp3val  10780  exp1  10784  expcl2lemap  10790  m1expcl2  10800  expaddzap  10822  sqcl  10839  nnsqcl  10848  qsqcl  10850  zesq  10897  facp1  10969  faccl  10974  facdiv  10977  bcval  10988  bcrpcl  10992  bcp1n  11000  bcpasc  11005  permnn  11010  hashennn  11019  hashcl  11020  lencl  11093  wrdexg  11100  elovmpowrd  11131  lswcl  11140  ccatcl  11146  ccatrn  11162  lswccatn0lsw  11164  ccatalpha  11166  s1cl  11174  swrdclg  11203  swrdwrdsymbg  11217  ccatswrd  11223  pfxval  11227  fnpfx  11230  pfxclg  11231  pfxwrdsymbg  11243  ccatpfx  11254  lenrevpfxcctswrd  11265  wrdind  11275  wrd2ind  11276  shftlem  11348  ovshftex  11351  shftf  11362  seq3shft  11370  cjth  11378  imval  11382  recl  11385  imcl  11386  crre  11389  remim  11392  reim0b  11394  cvg1nlemcau  11516  uzin2  11519  resqrexlem1arp  11537  resqrexlemp1rp  11538  resqrexlemglsq  11554  resqrexlemga  11555  resqrtcl  11561  abscl  11583  absrpclap  11593  nn0abscl  11617  fzomaxdiflem  11644  fzomaxdif  11645  maxabslemab  11738  maxcl  11742  zmaxcl  11756  minmax  11762  mincl  11763  xrmaxcl  11784  xrmaxaddlem  11792  xrminmax  11797  xrmincl  11798  xrmineqinf  11801  xrminrpcl  11806  reccn2ap  11845  climaddc1  11861  climmulc2  11863  climsubc1  11864  climsubc2  11865  climle  11866  climlec2  11873  climcvg1nlem  11881  sumrbdclem  11909  fsum3cvg  11910  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsumgcl  11918  fsum3  11919  isumss  11923  fisumss  11924  isumss2  11925  fsum3cvg2  11926  fsum3ser  11929  fsumcl2lem  11930  fsumcllem  11931  fsumadd  11938  sumsnf  11941  fsumsplitsn  11942  isumcl  11957  isummulc2  11958  isumrecl  11961  isumge0  11962  isumadd  11963  fsum2dlemstep  11966  fisumcom2  11970  mptfzshft  11974  fsumrev  11975  fsummulc2  11980  iserabs  12007  isumshft  12022  isumsplit  12023  isum1p  12024  isumrpcl  12026  isumle  12027  isumlessdc  12028  trireciplem  12032  expcnvap0  12034  expcnvre  12035  expcnv  12036  explecnv  12037  geolim  12043  geolim2  12044  geo2lim  12048  cvgratnnlemsumlt  12060  cvgratz  12064  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  prodf1f  12075  prodfdivap  12079  prodrbdclem  12103  fproddccvg  12104  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  fprodntrivap  12116  prodssdc  12121  fprodmul  12123  prodsnf  12124  fprodsplitdc  12128  fprodunsn  12136  fprodcl2lem  12137  fprodcllem  12138  fprodabs  12148  fprodrev  12151  fprod2dlemstep  12154  fprodcom2fi  12158  fprodsplitsn  12165  efcllemp  12190  ef0lem  12192  efcvgfsum  12199  reefcl  12200  ege2le3  12203  efcj  12205  efaddlem  12206  eftlcvg  12219  eftlcl  12220  reeftlcl  12221  eftlub  12222  efsep  12223  effsumlt  12224  efgt1p2  12227  efgt1p  12228  reeff1  12232  tanclap  12241  resincl  12252  recoscl  12253  retanclap  12254  eirraplem  12309  dvdsval2  12322  fsumdvds  12374  sqoddm1div8z  12418  bitsinv1lem  12493  gcdval  12501  gcdn0cl  12504  gcddvds  12505  divgcdnnr  12518  uzwodc  12579  nn0seqcvgd  12584  ialgrlem1st  12585  ialgrlemconst  12586  algrf  12588  algrp1  12589  eucalgf  12598  eucalglt  12600  lcmval  12606  lcmcllem  12610  lcmgcdlem  12620  cncongr2  12647  sqrt2irrlem  12704  oddpwdclemxy  12712  oddpwdclemdc  12716  qden1elz  12748  phicl2  12757  phimullem  12768  eulerthlemth  12775  prmdiv  12778  odzcllem  12786  pythagtriplem8  12816  pythagtriplem9  12817  pcval  12840  pczcl  12842  pcqcl  12850  dvdsprmpweqle  12881  pcaddlem  12883  pcmptcl  12886  pcmpt  12887  pockthlem  12900  pockthg  12901  zgz  12917  gznegcl  12919  gzcjcl  12920  gzaddcl  12921  gzmulcl  12922  gzabssqcl  12925  4sqlem5  12926  4sqlem4a  12935  mul4sqlem  12937  mul4sq  12938  4sqlemafi  12939  4sqlemffi  12940  4sqleminfi  12941  4sqexercise1  12942  4sqlem16  12950  4sqlem17  12951  ennnfonelemjn  12994  ennnfonelemg  12995  ennnfonelemp1  12998  ctinfomlemom  13019  ctiunctlemfo  13031  nninfdclemcl  13040  nninfdclemf  13041  nninfdclemp1  13042  setsex  13085  strsetsid  13086  strslfv3  13099  bassetsnn  13110  ressex  13119  ressbas2d  13122  strressid  13125  tgvalex  13317  ptex  13318  prdsex  13323  prdsval  13327  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfn  13371  imasaddval  13372  imasaddf  13373  imasmulfn  13374  imasmulval  13375  imasmulf  13376  qusval  13377  qusex  13379  qusaddvallemg  13387  qusaddflemg  13388  qusaddval  13389  qusaddf  13390  qusmulval  13391  qusmulf  13392  mgm1  13424  gsumress  13449  gsumprval  13453  prdsplusgsgrpcl  13468  prdsplusgcl  13500  prdsidlem  13501  pwsmnd  13504  mhmex  13516  subsubm  13537  0subm  13538  mhmeql  13546  gsumwsubmcl  13550  gsumfzcl  13553  grpsubval  13600  grplinv  13604  pwsgrp  13665  qusgrp2  13671  mulgval  13680  mulgex  13681  mulgfng  13682  mulg1  13687  mulgnnp1  13688  mulgnnsubcl  13692  mulgnn0subcl  13693  mulgsubcl  13694  mulgnndir  13709  subgex  13734  subgsubcl  13743  issubgrpd  13749  subsubg  13755  nsgconj  13764  0nsg  13772  triv1nsgd  13776  eqgex  13779  eqger  13782  eqgcpbl  13786  ghmex  13813  ghmpreima  13824  ghmnsgpreima  13827  conjnmz  13837  gsumfzsubmcl  13896  mgpex  13909  rngmgpf  13921  qusrng  13942  mgpf  13995  qusring2  14050  opprex  14057  opprrng  14061  opprring  14063  dvdsrex  14083  opprunitd  14095  dvrvald  14119  dvrcl  14120  unitdvcl  14121  invrpropdg  14134  subsubrng  14199  subrgcrng  14210  subrgsubm  14219  subrgugrp  14225  subsubrg  14230  rnrhmsubrg  14237  aprcotr  14270  rmodislmod  14336  lssvsubcl  14351  islss3  14364  lspex  14380  ellspsn  14402  sraex  14431  rlmlmod  14449  lidlex  14458  rspex  14459  lidl0cl  14468  lidlacl  14469  lidlnegcl  14470  ridl0  14495  ridl1  14496  2idlelbas  14501  cnsubglem  14564  expghmap  14592  mulgrhm  14594  zrhex  14606  znbaslemnn  14624  psrval  14651  psrbagfi  14658  psrbasg  14659  mplsubgfilemm  14683  mplsubgfilemcl  14684  mplsubgfileminv  14685  mplgrpfi  14691  iunopn  14697  toponmax  14720  tgtop  14763  tgiun  14768  tgidm  14769  ntropn  14812  tgrest  14864  restopnb  14876  cnovex  14891  cnclima  14918  txvalex  14949  txtop  14955  tx1cn  14964  tx2cn  14965  txcnp  14966  txcnmpt  14968  txdis1cn  14973  cnmptcom  14993  imasnopn  14994  hmeocnv  15002  hmeores  15010  txhmeo  15014  txswaphmeo  15016  ispsmet  15018  xmetres  15077  metres  15078  blex  15082  xmeter  15131  xmetresbl  15135  mopntopon  15138  isxms2  15147  xmetxp  15202  xmettx  15205  txmetcnp  15213  qtopbasss  15216  qtopbas  15217  reopnap  15241  ioo2blex  15247  blssioo  15248  tgioo  15249  fsumcncntop  15262  expcn  15264  cncfval  15267  divccncfap  15285  cdivcncfap  15299  divcncfap  15309  maxcncf  15310  mincncf  15311  ivthdec  15339  hoverb  15343  limccnpcntop  15370  dvrecap  15408  elplyd  15436  ply1termlem  15437  ply1term  15438  plymullem1  15443  plyaddlem  15444  plymullem  15445  plycolemc  15453  plyco  15454  plycj  15456  plycn  15457  plyreres  15459  dvply1  15460  dvply2g  15461  pilem3  15478  tanrpcl  15532  cosordlem  15544  ioocosf1o  15549  rpcncxpcl  15597  rpcxpcl  15598  rpabscxpbnd  15635  rplogbcl  15641  sgmnncl  15683  mpodvdsmulf1o  15685  fsumdvdsmul  15686  mersenne  15692  perfectlem2  15695  lgslem1  15700  lgsval  15704  lgscllem  15707  lgsne0  15738  gausslemma2dlem4  15764  lgseisenlem1  15770  lgsquadlem1  15777  lgsquadlem2  15778  2sqlem3  15817  2sqlem8  15823  vtxex  15840  iedgex  15841  edgvalg  15881  edgopval  15883  edgstruct  15885  usgrausgrien  15988  ausgrumgrien  15989  ausgrusgrien  15990  uspgr1ewopdc  16063  usgr2v1e2w  16065  vtxdgfif  16079  vtxdfifiun  16083  wlkex  16097  wlkelvv  16121  clwwlkccat  16170  djucllem  16273  012of  16470  2o01f  16471  nninfsellemeq  16494  qdencn  16509  cvgcmp2nlemabs  16514  trilpolemclim  16518  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523  nconstwlpolemgt0  16546