Theorem eqeltrid 2280

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

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

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 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eqeltrrid  2281  csbexga  4158  rabexd  4175  otexg  4260  tpexg  4476  dmresexg  4966  f1oabexg  5513  funfvex  5572  riotaexg  5878  riotaprop  5898  fnovex  5952  ovexg  5953  fovcdm  6063  fnovrn  6068  cofunexg  6163  cofunex2g  6164  abrexex2g  6174  xpexgALT  6187  mpofvex  6260  tfrex  6423  frec0g  6452  freccllem  6457  ecexg  6593  qsexg  6647  pmex  6709  elixpsn  6791  diffifi  6952  unfidisj  6980  prfidisj  6985  tpfidisj  6986  ssfirab  6992  ssfidc  6993  fnfi  6997  funrnfi  7003  iunfidisj  7007  infclti  7084  supex2g  7094  infex2g  7095  djuex  7104  ctssdccl  7172  addvalex  7906  negcl  8221  intqfrac2  10393  intfracq  10394  frec2uzzd  10474  frecuzrdgrrn  10482  iseqf1olemqpcl  10583  seq3f1olemqsum  10587  seqf1oglem1  10593  seqf1oglem2  10594  bcval5  10837  xrmaxiflemval  11396  climmpt  11446  reccn2ap  11459  zsumdc  11530  fsumzcl2  11551  fsump1i  11579  fsumabs  11611  hash2iun1dif1  11626  mertenslemi1  11681  fprodcllemf  11759  nninfctlemfo  12180  algrf  12186  algcvg  12189  algcvga  12192  algfx  12193  eucalgcvga  12199  eucalg  12200  crth  12365  phimullem  12366  eulerthlemth  12373  prmdiv  12376  pythagtriplem11  12415  pythagtriplem13  12417  pcprecl  12430  infpnlem1  12500  infpnlem2  12501  4sqlem5  12523  mul4sqlem  12534  4sqlemafi  12536  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  ennnfonelemj0  12561  ennnfonelemom  12568  ressbasid  12691  ressval3d  12693  1strbas  12738  2strbasg  12740  2stropg  12741  restid  12864  topnvalg  12865  topnidg  12866  imasival  12892  imasmulr  12895  imasaddfn  12903  imasaddval  12904  imasaddf  12905  imasmulfn  12906  imasmulval  12907  imasmulf  12908  qusval  12909  qusaddval  12921  qusaddf  12922  qusmulval  12923  qusmulf  12924  xpsval  12938  plusffvalg  12948  plusfvalg  12949  grpidvalg  12959  igsumvalx  12975  gsumfzval  12977  gsum0g  12982  gsumsplit1r  12984  gsumprval  12985  issubmnd  13026  ress0g  13027  ismhm  13036  0mhm  13061  grpinvfvalg  13117  grpinvval  13118  grpinvfng  13119  grpsubfvalg  13120  grpsubval  13121  grpressid  13136  grplactfval  13176  mulgfvalg  13194  mulgval  13195  mulgfng  13197  mulgnngsum  13200  mulgnnp1  13203  mulgnndir  13224  issubg  13246  subggrp  13250  issubg2m  13262  eqgfval  13295  eqgen  13300  quselbasg  13303  quseccl0g  13304  isghm  13316  ghmima  13338  ablressid  13408  gsumfzmptfidmadd  13412  mgpvalg  13422  mgpplusgg  13423  mgptopng  13428  mgpress  13430  rngressid  13453  issrg  13464  ringidss  13528  ring1  13558  ringressid  13562  opprvalg  13568  opprmulfvalg  13569  rdivmuldivd  13643  isnzr2  13683  issubrg  13720  subrgring  13723  rrgval  13761  islmod  13790  scaffvalg  13805  scafvalg  13806  lsssetm  13855  islssm  13856  islssmg  13857  lss1d  13882  lspfval  13887  lspval  13889  lspcl  13890  ellspsn  13916  rnglidlmmgm  13995  rnglidlmsgrp  13996  2idlval  14001  2idlvalg  14002  qusrhm  14027  zlmval  14126  zlmvscag  14132  znval  14135  znle  14136  znbaslemnn  14138  znbas  14143  znzrhval  14146  znleval  14152  psrval  14163  psrbasg  14170  psrelbas  14171  psrplusgg  14173  topopn  14187  topcld  14288  uncld  14292  iuncld  14294  unicld  14295  tgrest  14348  restin  14355  cnco  14400  cnrest  14414  cnptoprest2  14419  lmss  14425  txbasval  14446  txcn  14454  cnmpt12f  14465  hmeoco  14495  idhmeo  14496  blres  14613  metrest  14685  qtopbasss  14700  tgqioo  14734  divcnap  14744  fsumcncntop  14746  cncfmet  14771  sub1cncf  14781  sub2cncf  14782  cdivcncfap  14783  cnrehmeocntop  14789  cnplimcim  14846  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  dvfvalap  14860  dvidsslem  14872  dvmptfsum  14904  plyid  14925  gausslemma2dlem0b  15207  gausslemma2dlem0d  15209  gausslemma2dlem0h  15213  gausslemma2dlem5a  15222  gausslemma2dlem5  15223  gausslemma2dlem6  15224  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  2lgslem2  15249  2sqlem8  15280  bj-snexg  15474  trilpolemcl  15597