Theorem eqeltrid 2276

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eqeltrrid  2277  csbexga  4146  rabexd  4163  otexg  4248  tpexg  4462  dmresexg  4948  f1oabexg  5492  funfvex  5551  riotaexg  5856  riotaprop  5876  fnovex  5930  ovexg  5931  fovcdm  6040  fnovrn  6045  cofunexg  6135  cofunex2g  6136  abrexex2g  6146  xpexgALT  6159  mpofvex  6229  tfrex  6394  frec0g  6423  freccllem  6428  ecexg  6564  qsexg  6618  pmex  6680  elixpsn  6762  diffifi  6923  unfidisj  6951  prfidisj  6956  tpfidisj  6957  ssfirab  6963  ssfidc  6964  fnfi  6967  funrnfi  6972  iunfidisj  6976  infclti  7053  supex2g  7063  infex2g  7064  djuex  7073  ctssdccl  7141  addvalex  7874  negcl  8188  intqfrac2  10352  intfracq  10353  frec2uzzd  10433  frecuzrdgrrn  10441  iseqf1olemqpcl  10529  seq3f1olemqsum  10533  bcval5  10778  xrmaxiflemval  11293  climmpt  11343  reccn2ap  11356  zsumdc  11427  fsumzcl2  11448  fsump1i  11476  fsumabs  11508  hash2iun1dif1  11523  mertenslemi1  11578  fprodcllemf  11656  algrf  12080  algcvg  12083  algcvga  12086  algfx  12087  eucalgcvga  12093  eucalg  12094  crth  12259  phimullem  12260  eulerthlemth  12267  prmdiv  12270  pythagtriplem11  12309  pythagtriplem13  12311  pcprecl  12324  infpnlem1  12394  infpnlem2  12395  4sqlem5  12417  mul4sqlem  12428  4sqlemafi  12430  4sqlem13m  12438  4sqlem14  12439  4sqlem17  12442  4sqlem18  12443  ennnfonelemj0  12455  ennnfonelemom  12462  ressbasid  12585  ressval3d  12587  1strbas  12632  2strbasg  12634  2stropg  12635  restid  12758  topnvalg  12759  topnidg  12760  imasival  12786  imasmulr  12789  imasaddfn  12797  imasaddval  12798  imasaddf  12799  imasmulfn  12800  imasmulval  12801  imasmulf  12802  qusval  12803  qusaddval  12814  qusaddf  12815  qusmulval  12816  qusmulf  12817  xpsval  12831  plusffvalg  12841  plusfvalg  12842  grpidvalg  12852  igsumvalx  12868  gsum0g  12874  gsumsplit1r  12876  gsumprval  12877  issubmnd  12918  ress0g  12919  ismhm  12928  0mhm  12953  grpinvfvalg  13001  grpinvval  13002  grpinvfng  13003  grpsubfvalg  13004  grpsubval  13005  grpressid  13020  grplactfval  13060  mulgfvalg  13078  mulgval  13079  mulgfng  13081  mulgnngsum  13084  mulgnnp1  13087  mulgnndir  13108  issubg  13129  subggrp  13133  issubg2m  13145  eqgfval  13178  eqgen  13183  quselbasg  13186  quseccl0g  13187  isghm  13199  ghmima  13221  ablressid  13289  mgpvalg  13294  mgpplusgg  13295  mgptopng  13300  mgpress  13302  rngressid  13325  issrg  13336  ringidss  13400  ring1  13428  ringressid  13430  opprvalg  13436  opprmulfvalg  13437  rdivmuldivd  13511  issubrg  13585  subrgring  13588  islmod  13624  scaffvalg  13639  scafvalg  13640  lsssetm  13689  islssm  13690  islssmg  13691  lss1d  13716  lspfval  13721  lspval  13723  lspcl  13724  lspsnel  13750  rnglidlmmgm  13829  rnglidlmsgrp  13830  2idlvalg  13834  zlmval  13940  zlmvscag  13946  znval  13949  znle  13950  znbaslemnn  13952  znbas  13956  psrval  13961  psrbasg  13968  psrelbas  13969  psrplusgg  13971  topopn  13985  topcld  14086  uncld  14090  iuncld  14092  unicld  14093  tgrest  14146  restin  14153  cnco  14198  cnrest  14212  cnptoprest2  14217  lmss  14223  txbasval  14244  txcn  14252  cnmpt12f  14263  hmeoco  14293  idhmeo  14294  blres  14411  metrest  14483  qtopbasss  14498  tgqioo  14524  divcnap  14532  fsumcncntop  14533  cncfmet  14556  cdivcncfap  14564  cnrehmeocntop  14570  cnplimcim  14613  limccnpcntop  14621  limccnp2lem  14622  limccnp2cntop  14623  dvfvalap  14627  lgseisenlem1  14928  lgseisenlem2  14929  2sqlem8  14948  bj-snexg  15142  trilpolemcl  15264