Theorem eqeltrd 2281

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

Syntax hints:   → wi 4   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

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

This theorem is referenced by:  eqeltrrd  2282  3eltr4d  2288  eqeltrid  2291  eqeltrdi  2295  ifcldadc  3599  ifcldcd  3607  intab  3913  disjiun  4038  iinexgm  4197  opexg  4271  tfisi  4634  nnpredcl  4670  imain  5355  fvmptd  5659  fvmptdf  5666  fvmptt  5670  elfvmptrab  5674  dffo3  5726  resfunexg  5804  f1oiso2  5895  riota2df  5919  riota5f  5923  ovmpodxf  6070  ovmpodf  6076  offval  6165  ofvalg  6167  offeq  6171  iunexg  6203  oprabexd  6211  fo1stresm  6246  fo2ndresm  6247  oprssdmm  6256  1stdm  6267  1stconst  6306  2ndconst  6307  cnvf1olem  6309  fo2ndf  6312  f1od2  6320  iunon  6369  tfrlemibacc  6411  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembfn  6442  tfrcl  6449  rdgon  6471  frec0g  6482  freccllem  6487  frecfcllem  6489  frecsuclem  6491  oacl  6545  omcl  6546  oeicl  6547  nntr2  6588  mptelixpg  6820  fidifsnen  6966  en2eqpr  7003  unfiin  7022  tpfidceq  7026  ssfirab  7032  fnfi  7037  relcnvfi  7042  fidcenumlemr  7056  elfi2  7073  supclti  7099  supubti  7100  suplubti  7101  supelti  7103  ordiso2  7136  djulclr  7150  djurclr  7151  djulcl  7152  djurcl  7153  djuss  7171  updjudhcoinlf  7181  updjudhcoinrg  7182  ctssdclemn0  7211  ctssdccl  7212  ctssdc  7214  enumctlemm  7215  nninfwlpoimlemg  7276  cardcl  7287  exmidontriimlem2  7333  exmidapne  7371  cc2lem  7377  cc3  7379  addclpi  7439  mulclpi  7440  addclnq  7487  mulclnq  7488  addclnq0  7563  mulclnq0  7564  nqpnq0nq  7565  elnp1st2nd  7588  prarloclemcalc  7614  distrlem1prl  7694  distrlem1pru  7695  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  addcanprlemu  7727  recexprlemloc  7743  aptiprleml  7751  caucvgprprlemopl  7809  suplocexprlemex  7834  addclsr  7865  mulclsr  7866  recexgt0sr  7885  mulextsr1lem  7892  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  axaddcl  7976  axaddrcl  7977  axmulcl  7978  axmulrcl  7979  axcaucvglemval  8009  subcl  8270  cru  8674  aprcl  8718  aptap  8722  divclap  8750  redivclap  8803  diveqap1bd  8908  lbinfcl  9021  cju  9033  nn1m1nn  9053  nnsub  9074  nnnn0addcl  9324  un0addcl  9327  peano2z  9407  peano2zm  9409  zaddcllemneg  9410  zaddcl  9411  nnaddm1cl  9433  nn0n0n1ge2  9442  zdivadd  9461  zdivmul  9462  suprzclex  9470  zneo  9473  peano5uzti  9480  supinfneg  9715  infsupneg  9716  qmulz  9743  qnegcl  9756  qapne  9759  qdivcl  9763  cnref1o  9771  xnegcl  9953  xltnegi  9956  xaddnemnf  9978  xaddnepnf  9979  xnegdi  9989  xnpcan  9993  xltadd1  9997  xposdif  10003  xleaddadd  10008  iccf1o  10125  ige3m2fz  10170  ige2m1fz1  10230  zssinfcl  10373  infssuzex  10374  infssuzcldc  10376  zsupssdc  10379  suprzcl2dc  10380  rebtwn2z  10395  flqcl  10414  flapcl  10416  ceilqcl  10451  intfracq  10463  modqcl  10469  mulqmod0  10473  modqdifz  10479  zmodcl  10487  modfzo0difsn  10538  modsumfzodifsn  10539  frec2uzzd  10543  frec2uzsucd  10544  frec2uzuzd  10545  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdgrcl  10553  frecuzrdgsuc  10557  frecuzrdgrclt  10558  frecuzrdgg  10559  frecuzrdgsuctlem  10566  fzofig  10575  iseqovex  10601  seq3val  10603  seqvalcd  10604  seqf  10607  seqovcd  10610  seq3clss  10614  seq3caopr3  10634  iseqf1olemnab  10644  iseqf1olemqk  10650  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  iseqf1olemfvp  10653  seq3f1olemqsumkj  10654  seq3f1olemqsum  10656  seq3f1oleml  10659  seq3f1o  10660  seqf1oglem2a  10661  seqf1oglem1  10662  seqf1oglem2  10663  seq3distr  10675  ser0f  10677  ser3le  10680  exp3vallem  10683  exp3val  10684  exp1  10688  expcl2lemap  10694  m1expcl2  10704  expaddzap  10726  sqcl  10743  nnsqcl  10752  qsqcl  10754  zesq  10801  facp1  10873  faccl  10878  facdiv  10881  bcval  10892  bcrpcl  10896  bcp1n  10904  bcpasc  10909  permnn  10914  hashennn  10923  hashcl  10924  lencl  10996  wrdexg  11003  elovmpowrd  11033  lswcl  11042  ccatcl  11047  ccatrn  11063  lswccatn0lsw  11065  s1cl  11073  shftlem  11098  ovshftex  11101  shftf  11112  seq3shft  11120  cjth  11128  imval  11132  recl  11135  imcl  11136  crre  11139  remim  11142  reim0b  11144  cvg1nlemcau  11266  uzin2  11269  resqrexlem1arp  11287  resqrexlemp1rp  11288  resqrexlemglsq  11304  resqrexlemga  11305  resqrtcl  11311  abscl  11333  absrpclap  11343  nn0abscl  11367  fzomaxdiflem  11394  fzomaxdif  11395  maxabslemab  11488  maxcl  11492  zmaxcl  11506  minmax  11512  mincl  11513  xrmaxcl  11534  xrmaxaddlem  11542  xrminmax  11547  xrmincl  11548  xrmineqinf  11551  xrminrpcl  11556  reccn2ap  11595  climaddc1  11611  climmulc2  11613  climsubc1  11614  climsubc2  11615  climle  11616  climlec2  11623  climcvg1nlem  11631  sumrbdclem  11659  fsum3cvg  11660  summodclem3  11662  summodclem2a  11663  zsumdc  11666  fsumgcl  11668  fsum3  11669  isumss  11673  fisumss  11674  isumss2  11675  fsum3cvg2  11676  fsum3ser  11679  fsumcl2lem  11680  fsumcllem  11681  fsumadd  11688  sumsnf  11691  fsumsplitsn  11692  isumcl  11707  isummulc2  11708  isumrecl  11711  isumge0  11712  isumadd  11713  fsum2dlemstep  11716  fisumcom2  11720  mptfzshft  11724  fsumrev  11725  fsummulc2  11730  iserabs  11757  isumshft  11772  isumsplit  11773  isum1p  11774  isumrpcl  11776  isumle  11777  isumlessdc  11778  trireciplem  11782  expcnvap0  11784  expcnvre  11785  expcnv  11786  explecnv  11787  geolim  11793  geolim2  11794  geo2lim  11798  cvgratnnlemsumlt  11810  cvgratz  11814  mertenslemub  11816  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  prodf1f  11825  prodfdivap  11829  prodrbdclem  11853  fproddccvg  11854  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodntrivap  11866  prodssdc  11871  fprodmul  11873  prodsnf  11874  fprodsplitdc  11878  fprodunsn  11886  fprodcl2lem  11887  fprodcllem  11888  fprodabs  11898  fprodrev  11901  fprod2dlemstep  11904  fprodcom2fi  11908  fprodsplitsn  11915  efcllemp  11940  ef0lem  11942  efcvgfsum  11949  reefcl  11950  ege2le3  11953  efcj  11955  efaddlem  11956  eftlcvg  11969  eftlcl  11970  reeftlcl  11971  eftlub  11972  efsep  11973  effsumlt  11974  efgt1p2  11977  efgt1p  11978  reeff1  11982  tanclap  11991  resincl  12002  recoscl  12003  retanclap  12004  eirraplem  12059  dvdsval2  12072  fsumdvds  12124  sqoddm1div8z  12168  bitsinv1lem  12243  gcdval  12251  gcdn0cl  12254  gcddvds  12255  divgcdnnr  12268  uzwodc  12329  nn0seqcvgd  12334  ialgrlem1st  12335  ialgrlemconst  12336  algrf  12338  algrp1  12339  eucalgf  12348  eucalglt  12350  lcmval  12356  lcmcllem  12360  lcmgcdlem  12370  cncongr2  12397  sqrt2irrlem  12454  oddpwdclemxy  12462  oddpwdclemdc  12466  qden1elz  12498  phicl2  12507  phimullem  12518  eulerthlemth  12525  prmdiv  12528  odzcllem  12536  pythagtriplem8  12566  pythagtriplem9  12567  pcval  12590  pczcl  12592  pcqcl  12600  dvdsprmpweqle  12631  pcaddlem  12633  pcmptcl  12636  pcmpt  12637  pockthlem  12650  pockthg  12651  zgz  12667  gznegcl  12669  gzcjcl  12670  gzaddcl  12671  gzmulcl  12672  gzabssqcl  12675  4sqlem5  12676  4sqlem4a  12685  mul4sqlem  12687  mul4sq  12688  4sqlemafi  12689  4sqlemffi  12690  4sqleminfi  12691  4sqexercise1  12692  4sqlem16  12700  4sqlem17  12701  ennnfonelemjn  12744  ennnfonelemg  12745  ennnfonelemp1  12748  ctinfomlemom  12769  ctiunctlemfo  12781  nninfdclemcl  12790  nninfdclemf  12791  nninfdclemp1  12792  setsex  12835  strsetsid  12836  strslfv3  12849  ressex  12868  ressbas2d  12871  strressid  12874  tgvalex  13066  ptex  13067  prdsex  13072  prdsval  13076  imasex  13108  imasival  13109  imasbas  13110  imasplusg  13111  imasmulr  13112  imasaddfn  13120  imasaddval  13121  imasaddf  13122  imasmulfn  13123  imasmulval  13124  imasmulf  13125  qusval  13126  qusex  13128  qusaddvallemg  13136  qusaddflemg  13137  qusaddval  13138  qusaddf  13139  qusmulval  13140  qusmulf  13141  mgm1  13173  gsumress  13198  gsumprval  13202  prdsplusgsgrpcl  13217  prdsplusgcl  13249  prdsidlem  13250  pwsmnd  13253  mhmex  13265  subsubm  13286  0subm  13287  mhmeql  13295  gsumwsubmcl  13299  gsumfzcl  13302  grpsubval  13349  grplinv  13353  pwsgrp  13414  qusgrp2  13420  mulgval  13429  mulgex  13430  mulgfng  13431  mulg1  13436  mulgnnp1  13437  mulgnnsubcl  13441  mulgnn0subcl  13442  mulgsubcl  13443  mulgnndir  13458  subgex  13483  subgsubcl  13492  issubgrpd  13498  subsubg  13504  nsgconj  13513  0nsg  13521  triv1nsgd  13525  eqgex  13528  eqger  13531  eqgcpbl  13535  ghmex  13562  ghmpreima  13573  ghmnsgpreima  13576  conjnmz  13586  gsumfzsubmcl  13645  mgpex  13658  rngmgpf  13670  qusrng  13691  mgpf  13744  qusring2  13799  opprex  13806  opprrng  13810  opprring  13812  dvdsrex  13831  opprunitd  13843  dvrvald  13867  dvrcl  13868  unitdvcl  13869  invrpropdg  13882  subsubrng  13947  subrgcrng  13958  subrgsubm  13967  subrgugrp  13973  subsubrg  13978  rnrhmsubrg  13985  aprcotr  14018  rmodislmod  14084  lssvsubcl  14099  islss3  14112  lspex  14128  ellspsn  14150  sraex  14179  rlmlmod  14197  lidlex  14206  rspex  14207  lidl0cl  14216  lidlacl  14217  lidlnegcl  14218  ridl0  14243  ridl1  14244  2idlelbas  14249  cnsubglem  14312  expghmap  14340  mulgrhm  14342  zrhex  14354  znbaslemnn  14372  psrval  14399  psrbagfi  14406  psrbasg  14407  mplsubgfilemm  14431  mplsubgfilemcl  14432  mplsubgfileminv  14433  mplgrpfi  14439  iunopn  14445  toponmax  14468  tgtop  14511  tgiun  14516  tgidm  14517  ntropn  14560  tgrest  14612  restopnb  14624  cnovex  14639  cnclima  14666  txvalex  14697  txtop  14703  tx1cn  14712  tx2cn  14713  txcnp  14714  txcnmpt  14716  txdis1cn  14721  cnmptcom  14741  imasnopn  14742  hmeocnv  14750  hmeores  14758  txhmeo  14762  txswaphmeo  14764  ispsmet  14766  xmetres  14825  metres  14826  blex  14830  xmeter  14879  xmetresbl  14883  mopntopon  14886  isxms2  14895  xmetxp  14950  xmettx  14953  txmetcnp  14961  qtopbasss  14964  qtopbas  14965  reopnap  14989  ioo2blex  14995  blssioo  14996  tgioo  14997  fsumcncntop  15010  expcn  15012  cncfval  15015  divccncfap  15033  cdivcncfap  15047  divcncfap  15057  maxcncf  15058  mincncf  15059  ivthdec  15087  hoverb  15091  limccnpcntop  15118  dvrecap  15156  elplyd  15184  ply1termlem  15185  ply1term  15186  plymullem1  15191  plyaddlem  15192  plymullem  15193  plycolemc  15201  plyco  15202  plycj  15204  plycn  15205  plyreres  15207  dvply1  15208  dvply2g  15209  pilem3  15226  tanrpcl  15280  cosordlem  15292  ioocosf1o  15297  rpcncxpcl  15345  rpcxpcl  15346  rpabscxpbnd  15383  rplogbcl  15389  sgmnncl  15431  mpodvdsmulf1o  15433  fsumdvdsmul  15434  mersenne  15440  perfectlem2  15443  lgslem1  15448  lgsval  15452  lgscllem  15455  lgsne0  15486  gausslemma2dlem4  15512  lgseisenlem1  15518  lgsquadlem1  15525  lgsquadlem2  15526  2sqlem3  15565  2sqlem8  15571  djucllem  15698  012of  15892  2o01f  15893  nninfsellemeq  15913  qdencn  15928  cvgcmp2nlemabs  15933  trilpolemclim  15937  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  nconstwlpolemgt0  15965