Theorem eqeltrid 2294

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrid

Step	Hyp	Ref	Expression
1		eqeltrid.1	. . 3 |- A = B
2	1	a1i 9	. 2 |- ( ph -> A = B )
3		eqeltrid.2	. 2 |- ( ph -> B e. C )
4	2, 3	eqeltrd 2284	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

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

This theorem is referenced by:  eqeltrrid  2295  csbexga  4188  rabexd  4205  otexg  4292  tpexg  4509  dmresexg  5001  f1oabexg  5556  funfvex  5616  riotaexg  5926  riotaprop  5946  fnovex  6000  ovexg  6001  fovcdm  6112  fnovrn  6117  cofunexg  6217  cofunex2g  6218  abrexex2g  6228  xpexgALT  6241  mpofvex  6314  tfrex  6477  frec0g  6506  freccllem  6511  ecexg  6647  qsexg  6701  pmex  6763  elixpsn  6845  diffifi  7017  unfidisj  7045  prfidisj  7050  tpfidisj  7052  tpfidceq  7053  ssfirab  7059  ssfidc  7060  fnfi  7064  funrnfi  7070  iunfidisj  7074  infclti  7151  supex2g  7161  infex2g  7162  djuex  7171  ctssdccl  7239  addvalex  7992  negcl  8307  intqfrac2  10501  intfracq  10502  frec2uzzd  10582  frecuzrdgrrn  10590  iseqf1olemqpcl  10691  seq3f1olemqsum  10695  seqf1oglem1  10701  seqf1oglem2  10702  bcval5  10945  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12  11224  pfxccat3  11225  pfxccatpfx2  11228  pfxccat3a  11229  swrdccat3blem  11230  swrdccat3b  11231  xrmaxiflemval  11676  climmpt  11726  reccn2ap  11739  zsumdc  11810  fsumzcl2  11831  fsump1i  11859  fsumabs  11891  hash2iun1dif1  11906  mertenslemi1  11961  fprodcllemf  12039  bitsfzolem  12380  nninfctlemfo  12476  algrf  12482  algcvg  12485  algcvga  12488  algfx  12489  eucalgcvga  12495  eucalg  12496  crth  12661  phimullem  12662  eulerthlemth  12669  prmdiv  12672  pythagtriplem11  12712  pythagtriplem13  12714  pcprecl  12727  infpnlem1  12797  infpnlem2  12798  4sqlem5  12820  mul4sqlem  12831  4sqlemafi  12833  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  ennnfonelemj0  12887  ennnfonelemom  12894  ressbasid  13017  ressval3d  13019  1strbas  13064  2strbasg  13067  2stropg  13068  restid  13197  topnvalg  13198  topnidg  13199  prdsval  13220  prdsplusg  13224  prdsmulr  13225  pwsval  13238  pwselbasb  13240  pwssnf1o  13245  imasival  13253  imasmulr  13256  imasaddfn  13264  imasaddval  13265  imasaddf  13266  imasmulfn  13267  imasmulval  13268  imasmulf  13269  qusval  13270  qusaddval  13282  qusaddf  13283  qusmulval  13284  qusmulf  13285  xpsval  13299  plusffvalg  13309  plusfvalg  13310  grpidvalg  13320  igsumvalx  13336  gsumfzval  13338  gsum0g  13343  gsumsplit1r  13345  gsumprval  13346  prdssgrpd  13362  issubmnd  13389  ress0g  13390  ismhm  13408  0mhm  13433  grpinvfvalg  13489  grpinvval  13490  grpinvfng  13491  grpsubfvalg  13492  grpsubval  13493  grpressid  13508  grplactfval  13548  prdsinvlem  13555  mulgfvalg  13572  mulgval  13573  mulgfng  13575  mulgnngsum  13578  mulgnnp1  13581  mulgnndir  13602  issubg  13624  subggrp  13628  issubg2m  13640  eqgfval  13673  eqgen  13678  quselbasg  13681  quseccl0g  13682  isghm  13694  ghmima  13716  ablressid  13786  gsumfzmptfidmadd  13790  mgpvalg  13800  mgpplusgg  13801  mgptopng  13806  mgpress  13808  rngressid  13831  issrg  13842  ringidss  13906  ring1  13936  ringressid  13940  opprvalg  13946  opprmulfvalg  13947  rdivmuldivd  14021  isnzr2  14061  issubrg  14098  subrgring  14101  rrgval  14139  islmod  14168  scaffvalg  14183  scafvalg  14184  lsssetm  14233  islssm  14234  islssmg  14235  lss1d  14260  lspfval  14265  lspval  14267  lspcl  14268  ellspsn  14294  rnglidlmmgm  14373  rnglidlmsgrp  14374  2idlval  14379  2idlvalg  14380  qusrhm  14405  zlmval  14504  zlmvscag  14510  znval  14513  znle  14514  znbaslemnn  14516  znbas  14521  znzrhval  14524  znleval  14530  psrval  14543  psrbasg  14551  psrelbas  14552  psrplusgg  14555  mplvalcoe  14567  mplbascoe  14568  mplplusgg  14580  topopn  14595  topcld  14696  uncld  14700  iuncld  14702  unicld  14703  tgrest  14756  restin  14763  cnco  14808  cnrest  14822  cnptoprest2  14827  lmss  14833  txbasval  14854  txcn  14862  cnmpt12f  14873  hmeoco  14903  idhmeo  14904  blres  15021  metrest  15093  qtopbasss  15108  tgqioo  15142  divcnap  15152  fsumcncntop  15154  cncfmet  15179  sub1cncf  15189  sub2cncf  15190  cdivcncfap  15191  cnrehmeocntop  15197  cnplimcim  15254  limccnpcntop  15262  limccnp2lem  15263  limccnp2cntop  15264  dvfvalap  15268  dvidsslem  15280  dvmptfsum  15312  plyid  15333  fsumdvdsmul  15578  gausslemma2dlem0b  15642  gausslemma2dlem0d  15644  gausslemma2dlem0h  15648  gausslemma2dlem5a  15657  gausslemma2dlem5  15658  gausslemma2dlem6  15659  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  2lgslem2  15684  2sqlem8  15715  struct2slots2dom  15752  structiedg0val  15754  edgstruct  15775  uhgrunop  15798  incistruhgr  15801  upgrunop  15833  umgrunop  15835  bj-snexg  16047  trilpolemcl  16178