Theorem eqeltrid 2316

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 2306	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrid  2317  csbexga  4212  rabexd  4229  otexg  4316  tpexg  4535  dmresexg  5028  f1oabexg  5584  funfvex  5644  elfvex  5661  riotaexg  5958  riotaeqimp  5979  riotaprop  5980  fnovex  6034  ovexg  6035  elovimad  6045  fovcdm  6148  fnovrn  6153  cofunexg  6254  cofunex2g  6255  abrexex2g  6265  xpexgALT  6278  mpofvex  6351  tfrex  6514  frec0g  6543  freccllem  6548  ecexg  6684  qsexg  6738  pmex  6800  elixpsn  6882  diffifi  7056  unfidisj  7084  prfidisj  7089  tpfidisj  7091  tpfidceq  7092  ssfirab  7098  ssfidc  7099  fnfi  7103  funrnfi  7109  iunfidisj  7113  infclti  7190  supex2g  7200  infex2g  7201  djuex  7210  ctssdccl  7278  addvalex  8031  negcl  8346  intqfrac2  10541  intfracq  10542  frec2uzzd  10622  frecuzrdgrrn  10630  iseqf1olemqpcl  10731  seq3f1olemqsum  10735  seqf1oglem1  10741  seqf1oglem2  10742  bcval5  10985  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12  11265  pfxccat3  11266  pfxccatpfx2  11269  pfxccat3a  11270  swrdccat3blem  11271  swrdccat3b  11272  cats1cld  11295  xrmaxiflemval  11761  climmpt  11811  reccn2ap  11824  zsumdc  11895  fsumzcl2  11916  fsump1i  11944  fsumabs  11976  hash2iun1dif1  11991  mertenslemi1  12046  fprodcllemf  12124  bitsfzolem  12465  nninfctlemfo  12561  algrf  12567  algcvg  12570  algcvga  12573  algfx  12574  eucalgcvga  12580  eucalg  12581  crth  12746  phimullem  12747  eulerthlemth  12754  prmdiv  12757  pythagtriplem11  12797  pythagtriplem13  12799  pcprecl  12812  infpnlem1  12882  infpnlem2  12883  4sqlem5  12905  mul4sqlem  12916  4sqlemafi  12918  4sqlem13m  12926  4sqlem14  12927  4sqlem17  12930  4sqlem18  12931  ennnfonelemj0  12972  ennnfonelemom  12979  ressbasid  13103  ressval3d  13105  1strbas  13150  2strbasg  13153  2stropg  13154  restid  13283  topnvalg  13284  topnidg  13285  prdsval  13306  prdsplusg  13310  prdsmulr  13311  pwsval  13324  pwselbasb  13326  pwssnf1o  13331  imasival  13339  imasmulr  13342  imasaddfn  13350  imasaddval  13351  imasaddf  13352  imasmulfn  13353  imasmulval  13354  imasmulf  13355  qusval  13356  qusaddval  13368  qusaddf  13369  qusmulval  13370  qusmulf  13371  xpsval  13385  plusffvalg  13395  plusfvalg  13396  grpidvalg  13406  igsumvalx  13422  gsumfzval  13424  gsum0g  13429  gsumsplit1r  13431  gsumprval  13432  prdssgrpd  13448  issubmnd  13475  ress0g  13476  ismhm  13494  0mhm  13519  grpinvfvalg  13575  grpinvval  13576  grpinvfng  13577  grpsubfvalg  13578  grpsubval  13579  grpressid  13594  grplactfval  13634  prdsinvlem  13641  mulgfvalg  13658  mulgval  13659  mulgfng  13661  mulgnngsum  13664  mulgnnp1  13667  mulgnndir  13688  issubg  13710  subggrp  13714  issubg2m  13726  eqgfval  13759  eqgen  13764  quselbasg  13767  quseccl0g  13768  isghm  13780  ghmima  13802  ablressid  13872  gsumfzmptfidmadd  13876  mgpvalg  13886  mgpplusgg  13887  mgptopng  13892  mgpress  13894  rngressid  13917  issrg  13928  ringidss  13992  ring1  14022  ringressid  14026  opprvalg  14032  opprmulfvalg  14033  rdivmuldivd  14108  isnzr2  14148  issubrg  14185  subrgring  14188  rrgval  14226  islmod  14255  scaffvalg  14270  scafvalg  14271  lsssetm  14320  islssm  14321  islssmg  14322  lss1d  14347  lspfval  14352  lspval  14354  lspcl  14355  ellspsn  14381  rnglidlmmgm  14460  rnglidlmsgrp  14461  2idlval  14466  2idlvalg  14467  qusrhm  14492  zlmval  14591  zlmvscag  14597  znval  14600  znle  14601  znbaslemnn  14603  znbas  14608  znzrhval  14611  znleval  14617  psrval  14630  psrbasg  14638  psrelbas  14639  psrplusgg  14642  mplvalcoe  14654  mplbascoe  14655  mplplusgg  14667  topopn  14682  topcld  14783  uncld  14787  iuncld  14789  unicld  14790  tgrest  14843  restin  14850  cnco  14895  cnrest  14909  cnptoprest2  14914  lmss  14920  txbasval  14941  txcn  14949  cnmpt12f  14960  hmeoco  14990  idhmeo  14991  blres  15108  metrest  15180  qtopbasss  15195  tgqioo  15229  divcnap  15239  fsumcncntop  15241  cncfmet  15266  sub1cncf  15276  sub2cncf  15277  cdivcncfap  15278  cnrehmeocntop  15284  cnplimcim  15341  limccnpcntop  15349  limccnp2lem  15350  limccnp2cntop  15351  dvfvalap  15355  dvidsslem  15367  dvmptfsum  15399  plyid  15420  fsumdvdsmul  15665  gausslemma2dlem0b  15729  gausslemma2dlem0d  15731  gausslemma2dlem0h  15735  gausslemma2dlem5a  15744  gausslemma2dlem5  15745  gausslemma2dlem6  15746  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  2lgslem2  15771  2sqlem8  15802  struct2slots2dom  15839  structiedg0val  15841  edgstruct  15864  uhgrunop  15887  incistruhgr  15890  upgrunop  15925  umgrunop  15927  usgredg2v  16022  usgriedgdomord  16023  uspgredgdomord  16027  wksfval  16035  wlk1walkdom  16070  bj-snexg  16275  trilpolemcl  16405