Theorem eqeltrd 2242

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 2234	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mpbird 166	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eqeltrrd  2243  3eltr4d  2249  eqeltrid  2252  eqeltrdi  2256  ifcldadc  3548  ifcldcd  3554  intab  3852  disjiun  3976  iinexgm  4132  opexg  4205  tfisi  4563  nnpredcl  4599  imain  5269  fvmptd  5566  fvmptdf  5572  fvmptt  5576  elfvmptrab  5580  dffo3  5631  resfunexg  5705  f1oiso2  5794  riota2df  5817  riota5f  5821  ovmpodxf  5963  ovmpodf  5969  offval  6056  ofvalg  6058  offeq  6062  iunexg  6084  oprabexd  6092  fo1stresm  6126  fo2ndresm  6127  oprssdmm  6136  1stdm  6147  1stconst  6185  2ndconst  6186  cnvf1olem  6188  fo2ndf  6191  f1od2  6199  iunon  6248  tfrlemibacc  6290  tfrlemibfn  6292  tfr1onlembacc  6306  tfr1onlembfn  6308  tfrcllembacc  6319  tfrcllembfn  6321  tfrcl  6328  rdgon  6350  frec0g  6361  freccllem  6366  frecfcllem  6368  frecsuclem  6370  oacl  6424  omcl  6425  oeicl  6426  nntr2  6467  mptelixpg  6696  fidifsnen  6832  en2eqpr  6869  unfiin  6887  ssfirab  6895  fnfi  6898  relcnvfi  6902  fidcenumlemr  6916  elfi2  6933  supclti  6959  supubti  6960  suplubti  6961  supelti  6963  ordiso2  6996  djulclr  7010  djurclr  7011  djulcl  7012  djurcl  7013  djuss  7031  updjudhcoinlf  7041  updjudhcoinrg  7042  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  enumctlemm  7075  cardcl  7133  exmidontriimlem2  7174  cc2lem  7203  cc3  7205  addclpi  7264  mulclpi  7265  addclnq  7312  mulclnq  7313  addclnq0  7388  mulclnq0  7389  nqpnq0nq  7390  elnp1st2nd  7413  prarloclemcalc  7439  distrlem1prl  7519  distrlem1pru  7520  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  addcanprlemu  7552  recexprlemloc  7568  aptiprleml  7576  caucvgprprlemopl  7634  suplocexprlemex  7659  addclsr  7690  mulclsr  7691  recexgt0sr  7710  mulextsr1lem  7717  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axaddcl  7801  axaddrcl  7802  axmulcl  7803  axmulrcl  7804  axcaucvglemval  7834  subcl  8093  cru  8496  aprcl  8540  divclap  8570  redivclap  8623  diveqap1bd  8728  lbinfcl  8840  cju  8852  nn1m1nn  8871  nnsub  8892  nnnn0addcl  9140  un0addcl  9143  peano2z  9223  peano2zm  9225  zaddcllemneg  9226  zaddcl  9227  nnaddm1cl  9248  nn0n0n1ge2  9257  zdivadd  9276  zdivmul  9277  suprzclex  9285  zneo  9288  peano5uzti  9295  supinfneg  9529  infsupneg  9530  qmulz  9557  qnegcl  9570  qapne  9573  qdivcl  9577  cnref1o  9584  xnegcl  9764  xltnegi  9767  xaddnemnf  9789  xaddnepnf  9790  xnegdi  9800  xnpcan  9804  xltadd1  9808  xposdif  9814  xleaddadd  9819  iccf1o  9936  ige3m2fz  9980  ige2m1fz1  10040  rebtwn2z  10186  flqcl  10204  flapcl  10206  ceilqcl  10239  intfracq  10251  modqcl  10257  mulqmod0  10261  modqdifz  10267  zmodcl  10275  modfzo0difsn  10326  modsumfzodifsn  10327  frec2uzzd  10331  frec2uzsucd  10332  frec2uzuzd  10333  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  fzofig  10363  iseqovex  10387  seq3val  10389  seqvalcd  10390  seqf  10392  seqovcd  10394  seq3clss  10398  seq3caopr3  10412  iseqf1olemnab  10419  iseqf1olemqk  10425  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsum  10431  seq3f1oleml  10434  seq3f1o  10435  seq3distr  10444  ser0f  10446  ser3le  10449  exp3vallem  10452  exp3val  10453  exp1  10457  expcl2lemap  10463  m1expcl2  10473  expaddzap  10495  sqcl  10512  nnsqcl  10520  qsqcl  10522  zesq  10569  facp1  10639  faccl  10644  facdiv  10647  bcval  10658  bcrpcl  10662  bcp1n  10670  bcpasc  10675  permnn  10680  hashennn  10689  hashcl  10690  shftlem  10754  ovshftex  10757  shftf  10768  seq3shft  10776  cjth  10784  imval  10788  recl  10791  imcl  10792  crre  10795  remim  10798  reim0b  10800  cvg1nlemcau  10922  uzin2  10925  resqrexlem1arp  10943  resqrexlemp1rp  10944  resqrexlemglsq  10960  resqrexlemga  10961  resqrtcl  10967  abscl  10989  absrpclap  10999  nn0abscl  11023  fzomaxdiflem  11050  fzomaxdif  11051  maxabslemab  11144  maxcl  11148  zmaxcl  11162  minmax  11167  mincl  11168  xrmaxcl  11189  xrmaxaddlem  11197  xrminmax  11202  xrmincl  11203  xrmineqinf  11206  xrminrpcl  11211  reccn2ap  11250  climaddc1  11266  climmulc2  11268  climsubc1  11269  climsubc2  11270  climle  11271  climlec2  11278  climcvg1nlem  11286  sumrbdclem  11314  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  zsumdc  11321  fsumgcl  11323  fsum3  11324  isumss  11328  fisumss  11329  isumss2  11330  fsum3cvg2  11331  fsum3ser  11334  fsumcl2lem  11335  fsumcllem  11336  fsumadd  11343  sumsnf  11346  fsumsplitsn  11347  isumcl  11362  isummulc2  11363  isumrecl  11366  isumge0  11367  isumadd  11368  fsum2dlemstep  11371  fisumcom2  11375  mptfzshft  11379  fsumrev  11380  fsummulc2  11385  iserabs  11412  isumshft  11427  isumsplit  11428  isum1p  11429  isumrpcl  11431  isumle  11432  isumlessdc  11433  trireciplem  11437  expcnvap0  11439  expcnvre  11440  expcnv  11441  explecnv  11442  geolim  11448  geolim2  11449  geo2lim  11453  cvgratnnlemsumlt  11465  cvgratz  11469  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodf1f  11480  prodfdivap  11484  prodrbdclem  11508  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  fprodntrivap  11521  prodssdc  11526  fprodmul  11528  prodsnf  11529  fprodsplitdc  11533  fprodunsn  11541  fprodcl2lem  11542  fprodcllem  11543  fprodabs  11553  fprodrev  11556  fprod2dlemstep  11559  fprodcom2fi  11563  fprodsplitsn  11570  efcllemp  11595  ef0lem  11597  efcvgfsum  11604  reefcl  11605  ege2le3  11608  efcj  11610  efaddlem  11611  eftlcvg  11624  eftlcl  11625  reeftlcl  11626  eftlub  11627  efsep  11628  effsumlt  11629  efgt1p2  11632  efgt1p  11633  reeff1  11637  tanclap  11646  resincl  11657  recoscl  11658  retanclap  11659  eirraplem  11713  dvdsval2  11726  sqoddm1div8z  11819  zssinfcl  11877  infssuzex  11878  infssuzcldc  11880  zsupssdc  11883  suprzcl2dc  11884  gcdval  11888  gcdn0cl  11891  gcddvds  11892  divgcdnnr  11905  uzwodc  11966  nn0seqcvgd  11969  ialgrlem1st  11970  ialgrlemconst  11971  algrf  11973  algrp1  11974  eucalgf  11983  eucalglt  11985  lcmval  11991  lcmcllem  11995  lcmgcdlem  12005  cncongr2  12032  sqrt2irrlem  12089  oddpwdclemxy  12097  oddpwdclemdc  12101  qden1elz  12133  phicl2  12142  phimullem  12153  eulerthlemth  12160  prmdiv  12163  odzcllem  12170  pythagtriplem8  12200  pythagtriplem9  12201  pcval  12224  pczcl  12226  pcqcl  12234  dvdsprmpweqle  12264  pcaddlem  12266  pcmptcl  12268  pcmpt  12269  pockthlem  12282  pockthg  12283  zgz  12299  gznegcl  12301  gzcjcl  12302  gzaddcl  12303  gzmulcl  12304  gzabssqcl  12307  4sqlem5  12308  4sqlem4a  12317  mul4sqlem  12319  mul4sq  12320  ennnfonelemjn  12331  ennnfonelemg  12332  ennnfonelemp1  12335  ctinfomlemom  12356  ctiunctlemfo  12368  nninfdclemcl  12377  nninfdclemf  12378  nninfdclemp1  12379  setsex  12422  strsetsid  12423  ressid2  12449  ressval2  12450  ressid  12451  iunopn  12600  toponmax  12623  tgvalex  12650  tgtop  12668  tgiun  12673  tgidm  12674  ntropn  12717  tgrest  12769  restopnb  12781  cnovex  12796  cnclima  12823  txvalex  12854  txtop  12860  tx1cn  12869  tx2cn  12870  txcnp  12871  txcnmpt  12873  txdis1cn  12878  cnmptcom  12898  imasnopn  12899  hmeocnv  12907  hmeores  12915  txhmeo  12919  txswaphmeo  12921  ispsmet  12923  xmetres  12982  metres  12983  blex  12987  xmeter  13036  xmetresbl  13040  mopntopon  13043  isxms2  13052  xmetxp  13107  xmettx  13110  txmetcnp  13118  qtopbasss  13121  qtopbas  13122  reopnap  13138  ioo2blex  13144  blssioo  13145  tgioo  13146  fsumcncntop  13156  cncfval  13159  divccncfap  13177  cdivcncfap  13187  ivthdec  13222  limccnpcntop  13244  dvrecap  13277  pilem3  13304  tanrpcl  13358  cosordlem  13370  ioocosf1o  13375  rpcncxpcl  13423  rpcxpcl  13424  rpabscxpbnd  13459  rplogbcl  13464  lgslem1  13501  lgsval  13505  lgscllem  13508  lgsne0  13539  2sqlem3  13553  2sqlem8  13559  djucllem  13641  012of  13835  2o01f  13836  nninfsellemeq  13854  qdencn  13866  cvgcmp2nlemabs  13871  trilpolemclim  13875  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  nconstwlpolemgt0  13902