Theorem eqeltrid 2319

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

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

This theorem is referenced by:  eqeltrrid  2320  csbexga  4238  rabexd  4257  otexg  4346  tpexg  4565  dmresexg  5061  f1oabexg  5626  funfvex  5687  elfvfvex  5704  riotaexg  6007  riotaeqimp  6028  riotaprop  6029  fnovex  6083  ovexg  6084  elovimad  6094  fovcdm  6197  fnovrn  6202  cofunexg  6302  cofunex2g  6303  abrexex2g  6313  xpexgALT  6326  mpofvex  6401  mptsuppdifd  6455  tfrex  6599  frec0g  6628  freccllem  6633  ecexg  6771  qsexg  6825  pmex  6887  elixpsn  6970  diffifi  7151  unfidisj  7182  prfidisj  7187  tpfidisj  7189  tpfidceq  7190  ssfirab  7197  ssfidc  7198  fnfi  7203  funrnfi  7209  iunfidisj  7213  infclti  7314  supex2g  7324  infex2g  7325  djuex  7334  ctssdccl  7402  addvalex  8159  negcl  8473  intqfrac2  10681  intfracq  10682  frec2uzzd  10762  frecuzrdgrrn  10770  iseqf1olemqpcl  10871  seq3f1olemqsum  10875  seqf1oglem1  10881  seqf1oglem2  10882  bcval5  11125  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  pfxccat3  11426  pfxccatpfx2  11429  pfxccat3a  11430  swrdccat3blem  11431  swrdccat3b  11432  cats1cld  11455  xrmaxiflemval  11935  climmpt  11985  reccn2ap  11998  zsumdc  12070  fsumzcl2  12091  fsump1i  12119  fsumabs  12151  hash2iun1dif1  12166  mertenslemi1  12221  fprodcllemf  12299  bitsfzolem  12640  nninfctlemfo  12736  algrf  12742  algcvg  12745  algcvga  12748  algfx  12749  eucalgcvga  12755  eucalg  12756  crth  12921  phimullem  12922  eulerthlemth  12929  prmdiv  12932  pythagtriplem11  12972  pythagtriplem13  12974  pcprecl  12987  infpnlem1  13057  infpnlem2  13058  4sqlem5  13080  mul4sqlem  13091  4sqlemafi  13093  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  ennnfonelemj0  13152  ennnfonelemom  13159  ressbasid  13283  ressval3d  13285  1strbas  13330  2strbasg  13333  2stropg  13334  restid  13463  topnvalg  13464  topnidg  13465  prdsval  13486  prdsplusg  13490  prdsmulr  13491  pwsval  13504  pwselbasb  13506  pwssnf1o  13511  imasival  13519  imasmulr  13522  imasaddfn  13530  imasaddval  13531  imasaddf  13532  imasmulfn  13533  imasmulval  13534  imasmulf  13535  qusval  13536  qusaddval  13548  qusaddf  13549  qusmulval  13550  qusmulf  13551  xpsval  13565  plusffvalg  13575  plusfvalg  13576  grpidvalg  13586  igsumvalx  13602  gsumfzval  13604  gsum0g  13609  gsumsplit1r  13611  gsumprval  13612  prdssgrpd  13628  issubmnd  13655  ress0g  13656  ismhm  13674  0mhm  13699  grpinvfvalg  13755  grpinvval  13756  grpinvfng  13757  grpsubfvalg  13758  grpsubval  13759  grpressid  13774  grplactfval  13814  prdsinvlem  13821  mulgfvalg  13838  mulgval  13839  mulgfng  13841  mulgnngsum  13844  mulgnnp1  13847  mulgnndir  13868  issubg  13890  subggrp  13894  issubg2m  13906  eqgfval  13939  eqgen  13944  quselbasg  13947  quseccl0g  13948  isghm  13960  ghmima  13982  ablressid  14052  gsumfzmptfidmadd  14056  mgpvalg  14067  mgpplusgg  14068  mgptopng  14073  mgpress  14075  rngressid  14098  issrg  14109  ringidss  14173  ring1  14203  ringressid  14207  opprvalg  14213  opprmulfvalg  14214  rdivmuldivd  14289  isnzr2  14329  issubrg  14366  subrgring  14369  rrgval  14407  islmod  14439  scaffvalg  14454  scafvalg  14455  lsssetm  14504  islssm  14505  islssmg  14506  lss1d  14531  lspfval  14536  lspval  14538  lspcl  14539  ellspsn  14565  rnglidlmmgm  14644  rnglidlmsgrp  14645  2idlval  14650  2idlvalg  14651  qusrhm  14676  zlmval  14775  zlmvscag  14781  znval  14784  znle  14785  znbaslemnn  14787  znbas  14792  znzrhval  14795  znleval  14801  psrval  14814  psrbasg  14829  psrelbas  14830  psrplusgg  14833  mplvalcoe  14845  mplbascoe  14846  mplplusgg  14858  topopn  14873  topcld  14974  uncld  14978  iuncld  14980  unicld  14981  tgrest  15034  restin  15041  cnco  15086  cnrest  15100  cnptoprest2  15105  lmss  15111  txbasval  15132  txcn  15140  cnmpt12f  15151  hmeoco  15181  idhmeo  15182  blres  15299  metrest  15371  qtopbasss  15386  tgqioo  15420  divcnap  15430  fsumcncntop  15432  cncfmet  15457  sub1cncf  15467  sub2cncf  15468  cdivcncfap  15469  cnrehmeocntop  15475  cnplimcim  15532  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  dvfvalap  15546  dvidsslem  15558  dvmptfsum  15590  plyid  15611  fsumdvdsmul  15859  gausslemma2dlem0b  15923  gausslemma2dlem0d  15925  gausslemma2dlem0h  15929  gausslemma2dlem5a  15938  gausslemma2dlem5  15939  gausslemma2dlem6  15940  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  2lgslem2  15965  2sqlem8  15996  struct2slots2dom  16033  structiedg0val  16035  edgstruct  16059  uhgrunop  16082  incistruhgr  16085  upgrunop  16122  umgrunop  16124  usgredg2v  16219  usgriedgdomord  16220  uspgredgdomord  16224  subgruhgredgdm  16265  uhgrspansubgrlem  16271  uhgrspanop  16277  upgrspanop  16278  umgrspanop  16279  usgrspanop  16280  vtxdgfval  16283  wksfval  16317  wlk1walkdom  16354  clwwlkg  16388  trlsegvdeglem3  16457  trlsegvdeglem5  16459  eupthvdres  16470  eupth2lem3fi  16471  eupth2lembfi  16472  bj-snexg  16682  trilpolemcl  16821  gsumgfsumlem  16865  gfsumcl  16870