Theorem eqeltrid 2264

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrrid  2265  csbexga  4133  otexg  4232  tpexg  4446  dmresexg  4932  f1oabexg  5475  funfvex  5534  riotaexg  5837  riotaprop  5856  fnovex  5910  ovexg  5911  fovcdm  6019  fnovrn  6024  cofunexg  6112  cofunex2g  6113  abrexex2g  6123  xpexgALT  6136  mpofvex  6206  tfrex  6371  frec0g  6400  freccllem  6405  ecexg  6541  qsexg  6593  pmex  6655  elixpsn  6737  diffifi  6896  unfidisj  6923  prfidisj  6928  tpfidisj  6929  ssfirab  6935  ssfidc  6936  fnfi  6938  funrnfi  6943  iunfidisj  6947  infclti  7024  supex2g  7034  infex2g  7035  djuex  7044  ctssdccl  7112  addvalex  7845  negcl  8159  intqfrac2  10321  intfracq  10322  frec2uzzd  10402  frecuzrdgrrn  10410  iseqf1olemqpcl  10498  seq3f1olemqsum  10502  bcval5  10745  xrmaxiflemval  11260  climmpt  11310  reccn2ap  11323  zsumdc  11394  fsumzcl2  11415  fsump1i  11443  fsumabs  11475  hash2iun1dif1  11490  mertenslemi1  11545  fprodcllemf  11623  algrf  12047  algcvg  12050  algcvga  12053  algfx  12054  eucalgcvga  12060  eucalg  12061  crth  12226  phimullem  12227  eulerthlemth  12234  prmdiv  12237  pythagtriplem11  12276  pythagtriplem13  12278  pcprecl  12291  infpnlem1  12359  infpnlem2  12360  4sqlem5  12382  mul4sqlem  12393  ennnfonelemj0  12404  ennnfonelemom  12411  ressval3d  12533  1strbas  12578  2strbasg  12580  2stropg  12581  restid  12704  topnvalg  12705  topnidg  12706  imasival  12732  imasmulr  12735  imasaddfn  12743  imasaddval  12744  imasaddf  12745  imasmulfn  12746  imasmulval  12747  imasmulf  12748  qusval  12749  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  xpsval  12776  plusffvalg  12786  plusfvalg  12787  grpidvalg  12797  issubmnd  12848  ress0g  12849  ismhm  12858  0mhm  12878  grpinvfvalg  12920  grpinvval  12921  grpinvfng  12922  grpsubfvalg  12923  grpsubval  12924  grpressid  12936  grplactfval  12976  mulgfvalg  12990  mulgval  12991  mulgfng  12992  mulgnnp1  12996  mulgnndir  13017  issubg  13038  subggrp  13042  issubg2m  13054  eqgfval  13086  eqgen  13091  mgpvalg  13138  mgpplusgg  13139  mgptopng  13144  mgpress  13146  issrg  13153  ringidss  13217  ring1  13241  ringressid  13243  opprvalg  13246  opprmulfvalg  13247  rdivmuldivd  13318  issubrg  13347  subrgring  13350  islmod  13386  scaffvalg  13401  scafvalg  13402  lsssetm  13449  islssm  13450  lss1d  13475  topopn  13547  topcld  13648  uncld  13652  iuncld  13654  unicld  13655  tgrest  13708  restin  13715  cnco  13760  cnrest  13774  cnptoprest2  13779  lmss  13785  txbasval  13806  txcn  13814  cnmpt12f  13825  hmeoco  13855  idhmeo  13856  blres  13973  metrest  14045  qtopbasss  14060  tgqioo  14086  divcnap  14094  fsumcncntop  14095  cncfmet  14118  cdivcncfap  14126  cnrehmeocntop  14132  cnplimcim  14175  limccnpcntop  14183  limccnp2lem  14184  limccnp2cntop  14185  dvfvalap  14189  lgseisenlem1  14489  lgseisenlem2  14490  2sqlem8  14509  bj-snexg  14703  trilpolemcl  14824