Theorem eqeltrd 2247

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

Syntax hints:   -> wi 3   = wceq 1615   e. wcel 1617

This theorem is referenced by:  eqeltrrd 2248  syl5eqel 2251  syl5eqelOLD 2252  syl6eqel 2259  iinexg 3668  unisn2 3970  onuninsuci 4093  dffo3 4921  iunexg 4970  f1oiso2 5017  elimdeloprv 5062  fo1stres 5182  fo2ndres 5183  1stdm 5200  1stconst 5233  2ndconst 5234  omeulem1 5464  omxpenlem 5712  riotacl 5787  ordiso 5958  ordtypelem6 5964  tz9.12lem3 6059  rankon 6069  rankonOLD 6070  rankr1c 6078  rankxplim3 6126  cardid2 6173  oncardonOLD 6175  oncardid 6176  fodomnumlem 6273  cardcf 6338  cff1 6345  cflim2 6350  cfsmolem 6352  alephsing 6358  konigthlem 6504  konigthlemOLD 6506  addclpi 6615  mulclpi 6616  addclpq 6653  mulclpq 6655  addclsr 6787  mulclsr 6788  axaddopr 6860  axmulopr 6861  axaddrcl 6867  axmulrcl 6869  mulnzcnopr 7324  lbinfmcl 7706  infmrcl 7730  supxrbnd 7752  nn0addcl 7782  zdivadd 7853  zdivmul 7854  qdivcl 7912  flcl 7923  intfracq 7954  modcl 7960  zmodcl 7969  suprzcl 8111  seqzp1 8282  seq0p1 8285  seqzval2 8287  seqzalcl 8301  ser0cl1i 8307  sqcl 8356  recl 8507  imcl 8508  cjcl 8514  reim0b 8525  abscl 8584  caurei 8680  cauimi 8681  ser1absdiflem 8682  faccl 8693  facdiv 8695  bccl2 8724  permnn 8726  fz1fiOLD 8731  fsumcllem 8786  climaddlem3 8888  climaddc1 8890  climmullem8 8899  climmulc2 8901  climsub 8902  climsubc2 8903  climcmpc1 8911  climabslem 8920  caucvg3ai 8936  caucvg3lem 8938  iserzabslem 8950  cvgcmp2lem 8952  cvgcmp2clem 8954  cvgcmp2clemOLD 8955  cvgcmp3ci 8959  isumrecl 8983  isumcmpii 8988  supcvglem 8992  supcvglemOLD 8994  infcvglem2OLD 8999  infcvglem3OLD 9000  geolimilem 9013  divccncf 9058  isupivthi 9068  dsupivthlem 9069  dfef2i 9085  efcl 9090  reefcli 9095  efcji 9114  efaddlem6 9121  efaddlem26 9141  efaddlem27 9142  reeftlcl 9158  ef1tllem 9159  ef01tllem1 9161  ef01tllem2 9162  ef01tllem2OLD 9163  absef01tllem 9165  eirrlem2 9168  eirrlem3 9169  eirrlem4 9170  eirrlem5 9171  abspef01tlubi 9176  absefm1lei 9193  eflegeolem2 9195  sincl 9212  coscl 9213  resincl 9219  recoscl 9220  acdc3lem 9270  acdc2lem1 9273  acdc2lem2 9274  acdc5lem1 9276  acdc5lem2 9277  acdclem 9279  rpnnen1lem1 9289  gcdn0cl 9451  nn0seqcvgd 9469  eucalgf 9482  1arithlem14 9543  grpidcl 9633  grpinvcl 9642  ringidcl 9665  invrcl 9686  iunopn 9853  tpsexOLD 9861  istpsOLD 9862  tgval3 9896  tgtop 9899  basgen2 9910  indistop 9919  txtop 9942  icccld 9966  clint3OLD 9967  iincld 9968  clscld 9973  ntropn 9974  cmclsopn 9983  cmntrcld 9984  txcld 10002  idcn 10058  iscncl 10063  cnconst 10073  metres 10116  metxpcl 10125  lmfexlem2 10251  oprcn 10273  opr1cn 10274  opr2cn 10275  fsumcnlem 10285  bcthlem11 10305  bcthlem24 10318  bcthlem25 10319  grpoidcl 10364  grpoinvcl 10373  grpinvf 10385  gxcl 10409  issubgi 10452  readdsubg 10458  zaddsubg 10459  ablmul 10460  gaid 10475  ssga 10476  nvvc 10587  vacnlem4 10691  vacnlem6 10693  ipcl 10725  ip1cnilem5 10737  nmoxr 10789  siii 10877  minveclem17 10931  minveclem20 10934  minveclem22 10936  minveclem30 10944  minveclem31 10945  htthlem5 10998  spwcl 11030  efif 11102  effoi 11126  inficlALT 11205  tx1cn 11216  tx2cn 11217  uptx 11219  2txcn 11222  stoigOLD 11246  stoig 11247  filintf 11270  oefil2 11271  neifil 11298  fmf 11306  cncomp 11327  iorlid 11371  hvsubcl 11515  shsubcl 11715  hhssabli 11757  hhssnv 11759  axpjcl 11865  spancl 11929  hsupcl 11932  sshjcl 11952  spansnch 12108  hoscl 12146  homcl 12147  hodcl 12148  spansnscl 12218  3oalem2 12233  pjocini 12268  pjoi0 12287  mayete3i 12298  mayete3OLDi 12299  hococli 12318  nmopxr 12420  nmfnxr 12433  eigvalcl 12512  lnophm 12571  bdophmi 12589  cnlnadjlem2 12628  cnlnadjlem4 12630  cnlnadjlem5 12631  adjbdln 12643  adjbdlnb 12644  branmfn 12665  brabn 12666  rnbra 12667  pjcocli 12720  pjcohocli 12765  pj2cocli 12767  spansna 12911  atordi 12945  cdj3lem2a 12997  cdj3lem3a 13000  bnj1358 14012  addclnq 14548  mulclnq 14550  hashpwlem 14610  ghomgrpilem2 14613  circumlem3 14644  fseq1cl 14656  epsetlike 14795  axdense 14943  axfelem21 14966  cexint2OLD 15453  tolat 15631  toplat 15638  clfsebs 15703  seqzp2 15712  expus 15722  inttop4 15879  idhme 15897  hmphre 15902  qusp 15932  prtoptop 15945  rcfpfil 15961  stfincomp 15998  trhom 16022  tpgprop1 16025  tpgprop2 16026  ltrhom 16027  lrtrhom 16028  grphmlem1 16030  cntrsetlem 16052  mslb1 16060  2wsms 16061  supbrr 16103  dedalg 16145  aidm2 16152  catded 16166  dualalg 16186  isfuna 16237  idsubfun 16261  inficlALTOLD 16457  ordisoOLD 16459  ordtypelem6OLD 16465  hartog 16469  cnsubsp2 16512  isfne 16565  isref 16573  locfincomp 16599  comppfsc 16602  topmtcl 16610  topjoin 16612  ufileu 16658  filufint 16659  ufinffr 16663  filcon 16665  rnelfmlem 16677  rnelfm 16678  fmfnfmlem1 16679  fmfnfmlem2 16680  fmfnfmlem4 16682  fmfnfm 16683  filfm 16685  fcluscf 16697  filnetlem5 16729  filnet 16730  ifclda 16780  oprabexd 16798  upixp 16814  eroprf 16820  fdc 16897  incsequz2 16901  fsumltisumi 16908  fsumlt1 16916  mettrifi2 16933  geomcau 16934  lincmb01cmp 16963  lincmb01icc 16964  cnimass 16973  cnss 16977  paste 16978  piececn 16979  cncfres 16980  haustlmu 16991  tlmconst 16992  txcldOLD 16999  cnresoprab 17000  heiborlem11 17050  heiborlem33 17072  bfplem8 17090  icccmp 17112  phtpyid 17134  phtpycom 17135  phtpycolem3 17138  phtpycolem4 17139  phtpycolem5 17140  reparphtlem2 17149  reparpht 17150  pcocn 17161  pcoloopf 17164  pcohtpylem3 17167  pcoass 17170  pcorevlem 17171  pcorev 17172  pi1gp 17180  isringd 17182  isdivrng2 17196  idlnegcl 17255  idlsubcl 17256  igenidl 17296  lnnat 18087  2atm 18106  1cvrat 18137  2atmat 18265  2llnm2 18272  2lplnm2 18325  dalemrot 18361  dalemcea 18364  dalem2 18365  dalem14 18381  dalem23 18400  dath2 18442  pmapsub 18472  linepmap 18479  paddasslem11 18534  pmodlem1 18550  polsub 18596  paddatcl 18635  polsubcl 18637  osumcl 18652  trlcl 18796  4atexlemc 18826  trlat 18839  trlval3 18855  arglem1 18857  cdleme11h 18933  cdleme16d 18948  cdlemeda 18965  cdleme20l2 18989  cdleme27cl 19034  cdlemefrs29cl 19069  cdlemefr27cl 19073  cdlemefs27cl 19083  cdleme32fvcl 19112  cdleme48gfv 19218  cdleme51finvtr 19239  cdlemg1ltrnlem 19249  cdlemg1finvtrlem 19250  cdlemg1ci2 19257  cdlemg7fvbw 19283  cdlemg18d 19359  tgrpgrplem 19421  tendoco 19439  tendoplcl2 19443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1622  ax-17 1634  ax-4 1637  ax-5o 1639  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-an 435  df-ex 1645  df-cleq 2163  df-clel 2166

Copyright terms: Public domain