Theorem eqeltrd 2273

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrrd  2274  3eltr4d  2280  eqeltrid  2283  eqeltrdi  2287  ifcldadc  3591  ifcldcd  3598  intab  3904  disjiun  4029  iinexgm  4188  opexg  4262  tfisi  4624  nnpredcl  4660  imain  5341  fvmptd  5645  fvmptdf  5652  fvmptt  5656  elfvmptrab  5660  dffo3  5712  resfunexg  5786  f1oiso2  5877  riota2df  5901  riota5f  5905  ovmpodxf  6052  ovmpodf  6058  offval  6147  ofvalg  6149  offeq  6153  iunexg  6185  oprabexd  6193  fo1stresm  6228  fo2ndresm  6229  oprssdmm  6238  1stdm  6249  1stconst  6288  2ndconst  6289  cnvf1olem  6291  fo2ndf  6294  f1od2  6302  iunon  6351  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  tfrcl  6431  rdgon  6453  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  oacl  6527  omcl  6528  oeicl  6529  nntr2  6570  mptelixpg  6802  fidifsnen  6940  en2eqpr  6977  unfiin  6996  tpfidceq  7000  ssfirab  7006  fnfi  7011  relcnvfi  7016  fidcenumlemr  7030  elfi2  7047  supclti  7073  supubti  7074  suplubti  7075  supelti  7077  ordiso2  7110  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djuss  7145  updjudhcoinlf  7155  updjudhcoinrg  7156  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nninfwlpoimlemg  7250  cardcl  7261  exmidontriimlem2  7307  exmidapne  7345  cc2lem  7351  cc3  7353  addclpi  7413  mulclpi  7414  addclnq  7461  mulclnq  7462  addclnq0  7537  mulclnq0  7538  nqpnq0nq  7539  elnp1st2nd  7562  prarloclemcalc  7588  distrlem1prl  7668  distrlem1pru  7669  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  addcanprlemu  7701  recexprlemloc  7717  aptiprleml  7725  caucvgprprlemopl  7783  suplocexprlemex  7808  addclsr  7839  mulclsr  7840  recexgt0sr  7859  mulextsr1lem  7866  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axaddcl  7950  axaddrcl  7951  axmulcl  7952  axmulrcl  7953  axcaucvglemval  7983  subcl  8244  cru  8648  aprcl  8692  aptap  8696  divclap  8724  redivclap  8777  diveqap1bd  8882  lbinfcl  8995  cju  9007  nn1m1nn  9027  nnsub  9048  nnnn0addcl  9298  un0addcl  9301  peano2z  9381  peano2zm  9383  zaddcllemneg  9384  zaddcl  9385  nnaddm1cl  9406  nn0n0n1ge2  9415  zdivadd  9434  zdivmul  9435  suprzclex  9443  zneo  9446  peano5uzti  9453  supinfneg  9688  infsupneg  9689  qmulz  9716  qnegcl  9729  qapne  9732  qdivcl  9736  cnref1o  9744  xnegcl  9926  xltnegi  9929  xaddnemnf  9951  xaddnepnf  9952  xnegdi  9962  xnpcan  9966  xltadd1  9970  xposdif  9976  xleaddadd  9981  iccf1o  10098  ige3m2fz  10143  ige2m1fz1  10203  zssinfcl  10341  infssuzex  10342  infssuzcldc  10344  zsupssdc  10347  suprzcl2dc  10348  rebtwn2z  10363  flqcl  10382  flapcl  10384  ceilqcl  10419  intfracq  10431  modqcl  10437  mulqmod0  10441  modqdifz  10447  zmodcl  10455  modfzo0difsn  10506  modsumfzodifsn  10507  frec2uzzd  10511  frec2uzsucd  10512  frec2uzuzd  10513  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgsuctlem  10534  fzofig  10543  iseqovex  10569  seq3val  10571  seqvalcd  10572  seqf  10575  seqovcd  10578  seq3clss  10582  seq3caopr3  10602  iseqf1olemnab  10612  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsum  10624  seq3f1oleml  10627  seq3f1o  10628  seqf1oglem2a  10629  seqf1oglem1  10630  seqf1oglem2  10631  seq3distr  10643  ser0f  10645  ser3le  10648  exp3vallem  10651  exp3val  10652  exp1  10656  expcl2lemap  10662  m1expcl2  10672  expaddzap  10694  sqcl  10711  nnsqcl  10720  qsqcl  10722  zesq  10769  facp1  10841  faccl  10846  facdiv  10849  bcval  10860  bcrpcl  10864  bcp1n  10872  bcpasc  10877  permnn  10882  hashennn  10891  hashcl  10892  lencl  10958  wrdexg  10965  elovmpowrd  10995  shftlem  11000  ovshftex  11003  shftf  11014  seq3shft  11022  cjth  11030  imval  11034  recl  11037  imcl  11038  crre  11041  remim  11044  reim0b  11046  cvg1nlemcau  11168  uzin2  11171  resqrexlem1arp  11189  resqrexlemp1rp  11190  resqrexlemglsq  11206  resqrexlemga  11207  resqrtcl  11213  abscl  11235  absrpclap  11245  nn0abscl  11269  fzomaxdiflem  11296  fzomaxdif  11297  maxabslemab  11390  maxcl  11394  zmaxcl  11408  minmax  11414  mincl  11415  xrmaxcl  11436  xrmaxaddlem  11444  xrminmax  11449  xrmincl  11450  xrmineqinf  11453  xrminrpcl  11458  reccn2ap  11497  climaddc1  11513  climmulc2  11515  climsubc1  11516  climsubc2  11517  climle  11518  climlec2  11525  climcvg1nlem  11533  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  zsumdc  11568  fsumgcl  11570  fsum3  11571  isumss  11575  fisumss  11576  isumss2  11577  fsum3cvg2  11578  fsum3ser  11581  fsumcl2lem  11582  fsumcllem  11583  fsumadd  11590  sumsnf  11593  fsumsplitsn  11594  isumcl  11609  isummulc2  11610  isumrecl  11613  isumge0  11614  isumadd  11615  fsum2dlemstep  11618  fisumcom2  11622  mptfzshft  11626  fsumrev  11627  fsummulc2  11632  iserabs  11659  isumshft  11674  isumsplit  11675  isum1p  11676  isumrpcl  11678  isumle  11679  isumlessdc  11680  trireciplem  11684  expcnvap0  11686  expcnvre  11687  expcnv  11688  explecnv  11689  geolim  11695  geolim2  11696  geo2lim  11700  cvgratnnlemsumlt  11712  cvgratz  11716  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodf1f  11727  prodfdivap  11731  prodrbdclem  11755  fproddccvg  11756  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prodssdc  11773  fprodmul  11775  prodsnf  11776  fprodsplitdc  11780  fprodunsn  11788  fprodcl2lem  11789  fprodcllem  11790  fprodabs  11800  fprodrev  11803  fprod2dlemstep  11806  fprodcom2fi  11810  fprodsplitsn  11817  efcllemp  11842  ef0lem  11844  efcvgfsum  11851  reefcl  11852  ege2le3  11855  efcj  11857  efaddlem  11858  eftlcvg  11871  eftlcl  11872  reeftlcl  11873  eftlub  11874  efsep  11875  effsumlt  11876  efgt1p2  11879  efgt1p  11880  reeff1  11884  tanclap  11893  resincl  11904  recoscl  11905  retanclap  11906  eirraplem  11961  dvdsval2  11974  fsumdvds  12026  sqoddm1div8z  12070  bitsinv1lem  12145  gcdval  12153  gcdn0cl  12156  gcddvds  12157  divgcdnnr  12170  uzwodc  12231  nn0seqcvgd  12236  ialgrlem1st  12237  ialgrlemconst  12238  algrf  12240  algrp1  12241  eucalgf  12250  eucalglt  12252  lcmval  12258  lcmcllem  12262  lcmgcdlem  12272  cncongr2  12299  sqrt2irrlem  12356  oddpwdclemxy  12364  oddpwdclemdc  12368  qden1elz  12400  phicl2  12409  phimullem  12420  eulerthlemth  12427  prmdiv  12430  odzcllem  12438  pythagtriplem8  12468  pythagtriplem9  12469  pcval  12492  pczcl  12494  pcqcl  12502  dvdsprmpweqle  12533  pcaddlem  12535  pcmptcl  12538  pcmpt  12539  pockthlem  12552  pockthg  12553  zgz  12569  gznegcl  12571  gzcjcl  12572  gzaddcl  12573  gzmulcl  12574  gzabssqcl  12577  4sqlem5  12578  4sqlem4a  12587  mul4sqlem  12589  mul4sq  12590  4sqlemafi  12591  4sqlemffi  12592  4sqleminfi  12593  4sqexercise1  12594  4sqlem16  12602  4sqlem17  12603  ennnfonelemjn  12646  ennnfonelemg  12647  ennnfonelemp1  12650  ctinfomlemom  12671  ctiunctlemfo  12683  nninfdclemcl  12692  nninfdclemf  12693  nninfdclemp1  12694  setsex  12737  strsetsid  12738  strslfv3  12751  ressex  12770  ressbas2d  12773  strressid  12776  tgvalex  12967  ptex  12968  prdsex  12973  prdsval  12977  imasex  13009  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfn  13021  imasaddval  13022  imasaddf  13023  imasmulfn  13024  imasmulval  13025  imasmulf  13026  qusval  13027  qusex  13029  qusaddvallemg  13037  qusaddflemg  13038  qusaddval  13039  qusaddf  13040  qusmulval  13041  qusmulf  13042  mgm1  13074  gsumress  13099  gsumprval  13103  prdsplusgsgrpcl  13118  prdsplusgcl  13150  prdsidlem  13151  pwsmnd  13154  mhmex  13166  subsubm  13187  0subm  13188  mhmeql  13196  gsumwsubmcl  13200  gsumfzcl  13203  grpsubval  13250  grplinv  13254  pwsgrp  13315  qusgrp2  13321  mulgval  13330  mulgex  13331  mulgfng  13332  mulg1  13337  mulgnnp1  13338  mulgnnsubcl  13342  mulgnn0subcl  13343  mulgsubcl  13344  mulgnndir  13359  subgex  13384  subgsubcl  13393  issubgrpd  13399  subsubg  13405  nsgconj  13414  0nsg  13422  triv1nsgd  13426  eqgex  13429  eqger  13432  eqgcpbl  13436  ghmex  13463  ghmpreima  13474  ghmnsgpreima  13477  conjnmz  13487  gsumfzsubmcl  13546  mgpex  13559  rngmgpf  13571  qusrng  13592  mgpf  13645  qusring2  13700  opprex  13707  opprrng  13711  opprring  13713  dvdsrex  13732  opprunitd  13744  dvrvald  13768  dvrcl  13769  unitdvcl  13770  invrpropdg  13783  subsubrng  13848  subrgcrng  13859  subrgsubm  13868  subrgugrp  13874  subsubrg  13879  rnrhmsubrg  13886  aprcotr  13919  rmodislmod  13985  lssvsubcl  14000  islss3  14013  lspex  14029  ellspsn  14051  sraex  14080  rlmlmod  14098  lidlex  14107  rspex  14108  lidl0cl  14117  lidlacl  14118  lidlnegcl  14119  ridl0  14144  ridl1  14145  2idlelbas  14150  cnsubglem  14213  expghmap  14241  mulgrhm  14243  zrhex  14255  znbaslemnn  14273  psrval  14300  psrbagfi  14307  psrbasg  14308  mplsubgfilemm  14332  mplsubgfilemcl  14333  mplsubgfileminv  14334  mplgrpfi  14340  iunopn  14346  toponmax  14369  tgtop  14412  tgiun  14417  tgidm  14418  ntropn  14461  tgrest  14513  restopnb  14525  cnovex  14540  cnclima  14567  txvalex  14598  txtop  14604  tx1cn  14613  tx2cn  14614  txcnp  14615  txcnmpt  14617  txdis1cn  14622  cnmptcom  14642  imasnopn  14643  hmeocnv  14651  hmeores  14659  txhmeo  14663  txswaphmeo  14665  ispsmet  14667  xmetres  14726  metres  14727  blex  14731  xmeter  14780  xmetresbl  14784  mopntopon  14787  isxms2  14796  xmetxp  14851  xmettx  14854  txmetcnp  14862  qtopbasss  14865  qtopbas  14866  reopnap  14890  ioo2blex  14896  blssioo  14897  tgioo  14898  fsumcncntop  14911  expcn  14913  cncfval  14916  divccncfap  14934  cdivcncfap  14948  divcncfap  14958  maxcncf  14959  mincncf  14960  ivthdec  14988  hoverb  14992  limccnpcntop  15019  dvrecap  15057  elplyd  15085  ply1termlem  15086  ply1term  15087  plymullem1  15092  plyaddlem  15093  plymullem  15094  plycolemc  15102  plyco  15103  plycj  15105  plycn  15106  plyreres  15108  dvply1  15109  dvply2g  15110  pilem3  15127  tanrpcl  15181  cosordlem  15193  ioocosf1o  15198  rpcncxpcl  15246  rpcxpcl  15247  rpabscxpbnd  15284  rplogbcl  15290  sgmnncl  15332  mpodvdsmulf1o  15334  fsumdvdsmul  15335  mersenne  15341  perfectlem2  15344  lgslem1  15349  lgsval  15353  lgscllem  15356  lgsne0  15387  gausslemma2dlem4  15413  lgseisenlem1  15419  lgsquadlem1  15426  lgsquadlem2  15427  2sqlem3  15466  2sqlem8  15472  djucllem  15554  012of  15748  2o01f  15749  nninfsellemeq  15769  qdencn  15784  cvgcmp2nlemabs  15789  trilpolemclim  15793  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  nconstwlpolemgt0  15821