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  5586  funfvex  5646  elfvfvex  5663  riotaexg  5964  riotaeqimp  5985  riotaprop  5986  fnovex  6040  ovexg  6041  elovimad  6051  fovcdm  6154  fnovrn  6159  cofunexg  6260  cofunex2g  6261  abrexex2g  6271  xpexgALT  6284  mpofvex  6357  tfrex  6520  frec0g  6549  freccllem  6554  ecexg  6692  qsexg  6746  pmex  6808  elixpsn  6890  diffifi  7064  unfidisj  7095  prfidisj  7100  tpfidisj  7102  tpfidceq  7103  ssfirab  7109  ssfidc  7110  fnfi  7114  funrnfi  7120  iunfidisj  7124  infclti  7201  supex2g  7211  infex2g  7212  djuex  7221  ctssdccl  7289  addvalex  8042  negcl  8357  intqfrac2  10553  intfracq  10554  frec2uzzd  10634  frecuzrdgrrn  10642  iseqf1olemqpcl  10743  seq3f1olemqsum  10747  seqf1oglem1  10753  seqf1oglem2  10754  bcval5  10997  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12  11281  pfxccat3  11282  pfxccatpfx2  11285  pfxccat3a  11286  swrdccat3blem  11287  swrdccat3b  11288  cats1cld  11311  xrmaxiflemval  11777  climmpt  11827  reccn2ap  11840  zsumdc  11911  fsumzcl2  11932  fsump1i  11960  fsumabs  11992  hash2iun1dif1  12007  mertenslemi1  12062  fprodcllemf  12140  bitsfzolem  12481  nninfctlemfo  12577  algrf  12583  algcvg  12586  algcvga  12589  algfx  12590  eucalgcvga  12596  eucalg  12597  crth  12762  phimullem  12763  eulerthlemth  12770  prmdiv  12773  pythagtriplem11  12813  pythagtriplem13  12815  pcprecl  12828  infpnlem1  12898  infpnlem2  12899  4sqlem5  12921  mul4sqlem  12932  4sqlemafi  12934  4sqlem13m  12942  4sqlem14  12943  4sqlem17  12946  4sqlem18  12947  ennnfonelemj0  12988  ennnfonelemom  12995  ressbasid  13119  ressval3d  13121  1strbas  13166  2strbasg  13169  2stropg  13170  restid  13299  topnvalg  13300  topnidg  13301  prdsval  13322  prdsplusg  13326  prdsmulr  13327  pwsval  13340  pwselbasb  13342  pwssnf1o  13347  imasival  13355  imasmulr  13358  imasaddfn  13366  imasaddval  13367  imasaddf  13368  imasmulfn  13369  imasmulval  13370  imasmulf  13371  qusval  13372  qusaddval  13384  qusaddf  13385  qusmulval  13386  qusmulf  13387  xpsval  13401  plusffvalg  13411  plusfvalg  13412  grpidvalg  13422  igsumvalx  13438  gsumfzval  13440  gsum0g  13445  gsumsplit1r  13447  gsumprval  13448  prdssgrpd  13464  issubmnd  13491  ress0g  13492  ismhm  13510  0mhm  13535  grpinvfvalg  13591  grpinvval  13592  grpinvfng  13593  grpsubfvalg  13594  grpsubval  13595  grpressid  13610  grplactfval  13650  prdsinvlem  13657  mulgfvalg  13674  mulgval  13675  mulgfng  13677  mulgnngsum  13680  mulgnnp1  13683  mulgnndir  13704  issubg  13726  subggrp  13730  issubg2m  13742  eqgfval  13775  eqgen  13780  quselbasg  13783  quseccl0g  13784  isghm  13796  ghmima  13818  ablressid  13888  gsumfzmptfidmadd  13892  mgpvalg  13902  mgpplusgg  13903  mgptopng  13908  mgpress  13910  rngressid  13933  issrg  13944  ringidss  14008  ring1  14038  ringressid  14042  opprvalg  14048  opprmulfvalg  14049  rdivmuldivd  14124  isnzr2  14164  issubrg  14201  subrgring  14204  rrgval  14242  islmod  14271  scaffvalg  14286  scafvalg  14287  lsssetm  14336  islssm  14337  islssmg  14338  lss1d  14363  lspfval  14368  lspval  14370  lspcl  14371  ellspsn  14397  rnglidlmmgm  14476  rnglidlmsgrp  14477  2idlval  14482  2idlvalg  14483  qusrhm  14508  zlmval  14607  zlmvscag  14613  znval  14616  znle  14617  znbaslemnn  14619  znbas  14624  znzrhval  14627  znleval  14633  psrval  14646  psrbasg  14654  psrelbas  14655  psrplusgg  14658  mplvalcoe  14670  mplbascoe  14671  mplplusgg  14683  topopn  14698  topcld  14799  uncld  14803  iuncld  14805  unicld  14806  tgrest  14859  restin  14866  cnco  14911  cnrest  14925  cnptoprest2  14930  lmss  14936  txbasval  14957  txcn  14965  cnmpt12f  14976  hmeoco  15006  idhmeo  15007  blres  15124  metrest  15196  qtopbasss  15211  tgqioo  15245  divcnap  15255  fsumcncntop  15257  cncfmet  15282  sub1cncf  15292  sub2cncf  15293  cdivcncfap  15294  cnrehmeocntop  15300  cnplimcim  15357  limccnpcntop  15365  limccnp2lem  15366  limccnp2cntop  15367  dvfvalap  15371  dvidsslem  15383  dvmptfsum  15415  plyid  15436  fsumdvdsmul  15681  gausslemma2dlem0b  15745  gausslemma2dlem0d  15747  gausslemma2dlem0h  15751  gausslemma2dlem5a  15760  gausslemma2dlem5  15761  gausslemma2dlem6  15762  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  2lgslem2  15787  2sqlem8  15818  struct2slots2dom  15855  structiedg0val  15857  edgstruct  15880  uhgrunop  15903  incistruhgr  15906  upgrunop  15941  umgrunop  15943  usgredg2v  16038  usgriedgdomord  16039  uspgredgdomord  16043  vtxdgfval  16048  wksfval  16068  wlk1walkdom  16105  clwwlkg  16136  bj-snexg  16358  trilpolemcl  16493