Theorem eqeltrd 2315

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)

Hypotheses

Ref	Expression
eqeltrd.1	|- ( ph -> A = B )
eqeltrd.2	|- ( ph -> B e. C )

Assertion

Ref	Expression
eqeltrd	|- ( ph -> A e. C )

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 |- ( ph -> B e. C )
2		eqeltrd.1	. . 3 |- ( ph -> A = B )
3	2	eleq1d 2307	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A e. C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrd  2316  3eltr4d  2322  eqeltrid  2325  eqeltrdi  2329  ifcldadc  3670  ifcldcd  3678  intab  3999  disjiun  4125  iinexgm  4290  opexg  4368  tfisi  4734  nnpredcl  4770  opabssxpd  4811  imain  5463  fvmptd  5786  fvmptdf  5793  fvmptt  5797  elfvmptrab  5802  dffo3  5855  resfunexg  5936  f1oiso2  6033  riota2df  6060  riota5f  6065  ovmpodxf  6214  ovmpodf  6220  offval  6310  ofvalg  6312  offeq  6316  iunexg  6348  oprabexd  6360  fo1stresm  6395  fo2ndresm  6396  oprssdmm  6405  1stdm  6416  1stconst  6457  2ndconst  6458  cnvf1olem  6460  fo2ndf  6463  f1od2  6471  iunon  6555  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  tfrcl  6635  rdgon  6657  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  oacl  6733  omcl  6734  oeicl  6735  nntr2  6776  mptelixpg  7016  fidifsnen  7172  en2eqpr  7214  unfiin  7233  tpfidceq  7237  ssfirab  7244  fnfi  7250  relcnvfi  7255  fidcenumlemr  7272  snopfsuppdc  7299  fsuppcorn  7301  elfi2  7306  supclti  7338  supubti  7339  suplubti  7340  supelti  7342  ordiso2  7375  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djuss  7410  updjudhcoinlf  7420  updjudhcoinrg  7421  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nninfwlpoimlemg  7515  cardcl  7526  exmidontriimlem2  7578  exmidapne  7626  cc2lem  7632  cc3  7634  addclpi  7694  mulclpi  7695  addclnq  7742  mulclnq  7743  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  elnp1st2nd  7843  prarloclemcalc  7869  distrlem1prl  7949  distrlem1pru  7950  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprlemu  7982  recexprlemloc  7998  aptiprleml  8006  caucvgprprlemopl  8064  suplocexprlemex  8089  addclsr  8120  mulclsr  8121  recexgt0sr  8140  mulextsr1lem  8147  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axaddcl  8231  axaddrcl  8232  axmulcl  8233  axmulrcl  8234  axcaucvglemval  8264  subcl  8526  cru  8932  aprcl  8976  aptap  8980  divclap  9010  redivclap  9063  diveqap1bd  9168  lbinfcl  9281  cju  9293  nn1m1nn  9324  nnsub  9345  nnnn0addcl  9597  un0addcl  9600  peano2z  9684  peano2zm  9686  zaddcllemneg  9687  zaddcl  9688  nnaddm1cl  9710  nn0n0n1ge2  9719  zdivadd  9739  zdivmul  9740  suprzclex  9748  zneo  9751  peano5uzti  9758  supinfneg  10004  infsupneg  10005  qmulz  10032  qnegcl  10045  qapne  10048  qdivcl  10052  cnref1o  10061  xnegcl  10244  xltnegi  10247  xaddnemnf  10269  xaddnepnf  10270  xnegdi  10280  xnpcan  10284  xltadd1  10288  xposdif  10294  xleaddadd  10299  iccf1o  10417  ige3m2fz  10464  ige2m1fz1  10526  zssinfcl  10675  infssuzex  10676  infssuzcldc  10678  zsupssdc  10683  suprzcl2dc  10684  rebtwn2z  10699  flqcl  10718  flapclz  10720  ceilqcl  10758  intfracq  10770  modqcl  10776  mulqmod0  10780  modqdifz  10786  zmodcl  10794  modfzo0difsn  10845  modsumfzodifsn  10846  frec2uzzd  10850  frec2uzsucd  10851  frec2uzuzd  10852  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgsuctlem  10873  fzofig  10882  iseqovex  10908  seq3val  10910  seqvalcd  10911  seqf  10914  seqovcd  10917  seq3clss  10921  seq3caopr3  10941  iseqf1olemnab  10951  iseqf1olemqk  10957  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seq3f1oleml  10966  seq3f1o  10967  seqf1oglem2a  10968  seqf1oglem1  10969  seqf1oglem2  10970  seq3distr  10982  ser0f  10984  ser3le  10987  exp3vallem  10990  exp3val  10991  exp1  10995  expcl2lemap  11001  m1expcl2  11011  expaddzap  11033  sqcl  11050  nnsqcl  11059  qsqcl  11061  zesq  11109  facp1  11182  faccl  11187  facdiv  11190  bcval  11201  bcrpcl  11205  bcp1n  11213  bcpasc  11218  permnn  11224  hashennn  11233  hashcl  11234  hashf1  11301  lencl  11322  wrdexg  11329  elovmpowrd  11360  lswcl  11369  ccatcl  11375  ccatrn  11391  lswccatn0lsw  11393  ccatalpha  11395  s1cl  11403  swrdclg  11436  swrdwrdsymbg  11450  ccatswrd  11456  pfxval  11460  fnpfx  11463  pfxclg  11464  pfxwrdsymbg  11476  ccatpfx  11487  lenrevpfxcctswrd  11498  wrdind  11508  wrd2ind  11509  shftlem  11595  ovshftex  11598  shftf  11609  seq3shft  11617  cjth  11625  imval  11629  recl  11632  imcl  11633  crre  11636  remim  11639  reim0b  11641  cvg1nlemcau  11764  uzin2  11767  resqrexlem1arp  11785  resqrexlemp1rp  11786  resqrexlemglsq  11802  resqrexlemga  11803  resqrtcl  11809  abscl  11831  absrpclap  11841  qabscl  11857  nn0abscl  11866  fzomaxdiflem  11893  fzomaxdif  11894  maxabslemab  11987  maxcl  11991  zmaxcl  12005  minmax  12011  mincl  12012  zmincl  12020  xrmaxcl  12034  xrmaxaddlem  12042  xrminmax  12047  xrmincl  12048  xrmineqinf  12051  xrminrpcl  12056  reccn2ap  12095  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  climle  12116  climlec2  12123  climcvg1nlem  12131  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  zsumdc  12167  fsumgcl  12169  fsum3  12170  isumss  12174  fisumss  12175  isumss2  12176  fsum3cvg2  12177  fsum3ser  12180  fsumcl2lem  12181  fsumcllem  12182  fsumadd  12189  sumsnf  12192  fsumsplitsn  12193  isumcl  12208  isummulc2  12209  isumrecl  12212  isumge0  12213  isumadd  12214  fsum2dlemstep  12217  fisumcom2  12221  mptfzshft  12225  fsumrev  12226  fsummulc2  12231  iserabs  12258  isumshft  12273  isumsplit  12274  isum1p  12275  isumrpcl  12277  isumle  12278  isumlessdc  12279  trireciplem  12283  expcnvap0  12285  expcnvre  12286  expcnv  12287  explecnv  12288  geolim  12294  geolim2  12295  geo2lim  12299  cvgratnnlemsumlt  12311  cvgratz  12315  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodf1f  12326  prodfdivap  12330  prodrbdclem  12354  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodntrivap  12367  prodssdc  12372  fprodmul  12374  prodsnf  12375  fprodsplitdc  12379  fprodunsn  12387  fprodcl2lem  12388  fprodcllem  12389  fprodabs  12399  fprodrev  12402  fprod2dlemstep  12405  fprodcom2fi  12409  fprodsplitsn  12416  efcllemp  12441  ef0lem  12443  efcvgfsum  12450  reefcl  12451  ege2le3  12454  efcj  12456  efaddlem  12457  eftlcvg  12470  eftlcl  12471  reeftlcl  12472  eftlub  12473  efsep  12474  effsumlt  12475  efgt1p2  12478  efgt1p  12479  reeff1  12483  tanclap  12492  resincl  12503  recoscl  12504  retanclap  12505  eirraplem  12560  dvdsval2  12573  fsumdvds  12625  sqoddm1div8z  12669  bitsinv1lem  12744  gcdval  12752  gcdn0cl  12755  gcddvds  12756  divgcdnnr  12769  uzwodc  12830  nn0seqcvgd  12835  ialgrlem1st  12836  ialgrlemconst  12837  algrf  12839  algrp1  12840  eucalgf  12849  eucalglt  12851  lcmval  12857  lcmcllem  12861  lcmgcdlem  12871  cncongr2  12898  sqrt2irrlem  12956  nnmaxpwlemxy  12964  nnmaxpwlemparts  12968  qden1elz  13001  nn0sqdcq  13004  sqrtrirr  13005  phicl2  13012  phimullem  13023  eulerthlemth  13030  prmdiv  13033  odzcllem  13041  pythagtriplem8  13071  pythagtriplem9  13072  pcval  13095  pczcl  13097  pcqcl  13105  dvdsprmpweqle  13136  pcaddlem  13138  pcmptcl  13141  pcmpt  13142  pockthlem  13155  pockthg  13156  zgz  13172  gznegcl  13174  gzcjcl  13175  gzaddcl  13176  gzmulcl  13177  gzabssqcl  13180  4sqlem5  13181  4sqlem4a  13190  mul4sqlem  13192  mul4sq  13193  4sqlemafi  13194  4sqlemffi  13195  4sqleminfi  13196  4sqexercise1  13197  4sqlem16  13205  4sqlem17  13206  ballotfilemfelz  13279  ballotfilemiex  13293  ballotfilemsdom  13304  ballotfilemgval  13316  ennnfonelemjn  13342  ennnfonelemg  13343  ennnfonelemp1  13346  ctinfomlemom  13367  ctiunctlemfo  13379  nninfdclemcl  13388  nninfdclemf  13389  nninfdclemp1  13390  setsex  13433  strsetsid  13434  strslfv3  13447  bassetsnn  13458  ressex  13468  ressbas2d  13471  strressid  13474  tgvalex  13666  ptex  13667  imasex  13675  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  imasaddfn  13687  imasaddval  13688  imasaddf  13689  imasmulfn  13690  imasmulval  13691  imasmulf  13692  qusval  13693  qusex  13695  qusaddvallemg  13703  qusaddflemg  13704  qusaddval  13705  qusaddf  13706  qusmulval  13707  qusmulf  13708  mgm1  13739  gzsumress  13761  mhmex  13818  subsubm  13839  0subm  13840  mhmeql  13848  gzsumwsubmcl  13850  gzsumcl  13853  grpsubval  13900  grplinv  13904  qusgrp2  13965  mulgval  13974  mulgex  13975  mulgfng  13976  mulg1  13981  mulgnnp1  13982  mulgnnsubcl  13986  mulgnn0subcl  13987  mulgsubcl  13988  mulgnndir  14003  subgex  14028  subgsubcl  14037  issubgrpd  14043  subsubg  14049  nsgconj  14058  0nsg  14066  triv1nsgd  14070  eqgex  14073  eqger  14076  eqgcpbl  14080  ghmex  14107  ghmpreima  14118  ghmnsgpreima  14121  conjnmz  14131  gzsumsubmcl  14191  gzsumsplit0  14197  gsumvalfi  14201  gsumsncmn  14205  gsumclfi  14208  gsumsubmclfi  14212  prdsex  14221  prdsval  14222  prdsplusgsgrpcl  14239  prdsplusgcl  14241  prdsidlem  14242  pwsmnd  14261  pwsgrp  14263  mgpex  14272  rngmgpf  14285  qusrng  14306  mgpf  14364  qusring2  14420  opprex  14427  opprrng  14431  opprring  14433  dvdsrex  14454  opprunitd  14466  dvrvald  14490  dvrcl  14491  unitdvcl  14492  invrpropdg  14505  subsubrng  14571  subrgcrng  14582  subrgsubm  14591  subrgugrp  14597  subsubrg  14602  rnrhmsubrg  14609  aprcotr  14646  aprnzr  14648  aprlring  14649  rmodislmod  14737  lssvsubcl  14752  islss3  14765  lspex  14781  ellspsn  14803  sraex  14832  rlmlmod  14850  lidlex  14859  rspex  14860  lidl0cl  14869  lidlacl  14870  lidlnegcl  14871  ridl0  14896  ridl1  14897  2idlelbas  14902  cnsubglem  14965  expghmap  14991  mulgrhm  14993  zrhex  15005  znbaslemnn  15023  asplss  15065  aspsubrg  15067  psrval  15099  psrbagfi  15108  psrbagcon  15111  psrbasg  15114  mplsubgfilemm  15138  mplsubgfilemcl  15139  mplsubgfileminv  15140  mplgrpfi  15146  iunopn  15152  toponmax  15175  tgtop  15218  tgiun  15223  tgidm  15224  ntropn  15267  tgrest  15319  restopnb  15331  cnovex  15346  cnclima  15373  txvalex  15404  txtop  15410  tx1cn  15419  tx2cn  15420  txcnp  15421  txcnmpt  15423  txdis1cn  15428  cnmptcom  15448  imasnopn  15449  hmeocnv  15457  hmeores  15465  txhmeo  15469  txswaphmeo  15471  ispsmet  15473  xmetres  15532  metres  15533  blex  15537  xmeter  15586  xmetresbl  15590  mopntopon  15593  isxms2  15602  xmetxp  15657  xmettx  15660  txmetcnp  15668  qtopbasss  15671  qtopbas  15672  reopnap  15696  ioo2blex  15702  blssioo  15703  tgioo  15704  fsumcncntop  15717  expcn  15719  cncfval  15722  divccncfap  15740  cdivcncfap  15754  divcncfap  15764  maxcncf  15765  mincncf  15766  ivthdec  15794  hoverb  15798  limccnpcntop  15825  dvrecap  15863  elplyd  15891  ply1termlem  15892  ply1term  15893  plymullem1  15898  plyaddlem  15899  plymullem  15900  plycolemc  15908  plyco  15909  plycj  15911  plycn  15912  plyreres  15914  dvply1  15915  dvply2g  15916  pilem3  15934  tanrpcl  15988  cosordlem  16000  ioocosf1o  16005  logfac  16048  rpcncxpcl  16057  rpcxpcl  16058  rpabscxpbnd  16095  rplogbcl  16101  zprmlogbaplem2  16135  log2tlbndlog2  16139  birthdaylem1g  16144  pellexlem1  16148  ppiqfi  16158  ppiqcl  16163  sgmnncl  16169  mpodvdsmulf1o  16185  fsumdvdsmul  16186  mersenne  16195  perfectlem2  16198  bposlem5  16213  lgslem1  16217  lgsval  16221  lgscllem  16224  lgsne0  16255  gausslemma2dlem4  16281  lgseisenlem1  16287  lgsquadlem1  16294  lgsquadlem2  16295  2sqlem3  16334  2sqlem8  16340  vtxex  16357  iedgex  16358  edgvalg  16398  edgopval  16401  edgstruct  16403  usgrausgrien  16508  ausgrumgrien  16509  ausgrusgrien  16510  uspgr1ewopdc  16583  usgr2v1e2w  16585  uhgrspansubgrlem  16615  vtxdgfif  16632  vtxdfifiun  16636  1loopgrvd2fi  16644  1loopgrvd0fi  16645  1hevtxdg0fi  16646  1hevtxdg1en  16647  p1evtxdeqfilem  16650  vdegp1bid  16654  wlkex  16664  wlkelvv  16688  clwwlkccat  16740  clwwlknonex2lem1  16776  clwwlknonex2lem2  16777  clwwlknonex2  16778  trlsegvdeglem6  16804  trlsegvdeglem7  16805  trlsegvdegfi  16806  eupth2lem3lem1fi  16807  eupth2lem3lem2fi  16808  eupth2lem3lem5  16811  eupth2lembfi  16816  eulerpathprum  16819  depindlem1  16845  depindlem2  16846  djucllem  16926  012of  17121  2o01f  17122  nninfsellemeq  17155  qdencn  17170  cvgcmp2nlemabs  17179  trilpolemclim  17183  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  nconstwlpolemgt0  17212