Theorem syl5eqelr 2536

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl5eqelr.1	|- B = A
syl5eqelr.2	|- ( ph -> B e. C )

Assertion

Ref	Expression
syl5eqelr	|- ( ph -> A e. C )

Proof of Theorem syl5eqelr

Step	Hyp	Ref	Expression
1		syl5eqelr.1	. . 3 |- B = A
2	1	eqcomi 2462	. 2 |- A = B
3		syl5eqelr.2	. 2 |- ( ph -> B e. C )
4	2, 3	syl5eqel 2535	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1446   e. wcel 1889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1666  df-cleq 2446  df-clel 2449

This theorem is referenced by:  3eltr3g  2547  dmrnssfld  5096  opabbrexOLD  6338  oprssdm  6455  offval  6543  cnvexg  6744  resfunexgALT  6761  abrexexg  6773  abrexex2g  6775  opabex3d  6776  suppssov1  6952  suppssfv  6956  ralxpmap  7526  imafi  7872  abrexfi  7879  ssfii  7938  wdomima2g  8106  unxpwdom2  8108  tskwe  8389  ac10ct  8470  fin23lem28  8775  fin23lem30  8777  axcclem  8892  distrlem4pr  9456  iccshftr  11773  iccshftl  11775  iccdil  11777  icccntr  11779  o1res  13636  exprmfct  14660  infpnlem1  14866  4sqlem13OLD  14913  4sqlem13  14919  0ram  14990  ressval3d  15198  ismred2  15521  mreexexlem2d  15563  mreexexlem4d  15565  acsfn1c  15580  acsfn2  15581  ssclem  15736  submacs  16624  efgrcl  17377  dprd2da  17687  srgbinom  17790  irredlmul  17948  lidlrsppropd  18466  issubassa  18560  ply1crng  18803  ply1ring  18853  ply1lmod  18857  chrcl  19109  css1  19265  oftpos  19489  tposmap  19494  0opn  19946  fctop2  20032  difopn  20061  tgrest  20187  ordtbas2  20219  ordtopn3  20224  ordtcld3  20227  t1ficld  20355  resthauslem  20391  kgentopon  20565  txbasex  20593  txcnpi  20635  txdis1cn  20662  pthaus  20665  txkgen  20679  cnmptid  20688  cnmptc  20689  cnmpt1st  20695  cnmpt2nd  20696  cnmpt2c  20697  cnmptkc  20706  txcon  20716  hmeoima  20792  hmeocld  20794  xkohmeo  20842  filufint  20947  fin1aufil  20959  flftg  21023  ptcmplem2  21080  tmdmulg  21119  tmdgsum2  21123  symgtgp  21128  submtmd  21131  ghmcnp  21141  qustgpopn  21146  qustgplem  21147  ust0  21246  nrginvrcn  21706  fsumcn  21914  fsum2cn  21915  expcn  21916  cnheibor  21995  evth2  22000  csscld  22232  clsocv  22233  ovoliun2  22471  volfiniun  22512  dyadmbl  22570  mbfeqalem  22610  mbfss  22614  ismbf3d  22622  mbfadd  22629  i1f0rn  22652  mbfmul  22696  itg2seq  22712  itg2monolem2  22721  itg2monolem3  22722  itg2mono  22723  itgreval  22766  itgge0  22780  itgss3  22784  iblconst  22787  itgconst  22788  ibladdlem  22789  itgfsum  22796  iblabslem  22797  itgabs  22804  mvth  22956  lhop1lem  22977  dvfsumle  22985  dvfsumlem2  22991  ftc1lem4  23003  itgparts  23011  itgsubstlem  23012  itgsubst  23013  plydivlem1  23258  aannenlem1  23296  taylply2  23335  itgulm  23375  cxpcn  23697  resqrtcn  23701  basellem1  24019  mulogsumlem  24381  mulog2sumlem2  24385  selberg2lem  24400  pntrsumo1  24415  nbgracnvfv  25180  zrdivrng  26172  pjssmii  27346  abrexexd  28155  ogrpaddltrbid  28496  lmatfval  28652  pl1cn  28773  esumcvg  28919  esumcvgsum  28921  sigaval  28944  sigaclfu2  28955  sigapildsys  28996  ldgenpisys  29000  measinb2  29057  braew  29077  unelcarsg  29156  carsgclctunlem2  29163  sibfof  29185  sitgclg  29187  orrvcoel  29310  orrvccel  29311  subfaclefac  29911  cvmsss2  30009  cvmopnlem  30013  mpstrcl  30191  elmpps  30223  hmeoclda  31001  bj-1uplex  31614  bj-2uplex  31628  bj-diagval  31657  icoreclin  31772  broucube  31986  mblfinlem1  31989  cnambfre  32001  ibladdnclem  32010  iblabsnclem  32017  itgabsnc  32023  ftc1cnnclem  32027  ftc1anclem4  32032  ftc1anclem5  32033  ftc1anclem6  32034  ftc1anclem7  32035  ftc2nc  32038  areacirc  32049  dalemrot  33234  dalem10  33250  arglem1N  33768  cdlemk36  34492  mzpconstmpt  35594  mzpresrename  35604  diophrex  35630  0dioph  35633  anrabdioph  35635  orrabdioph  35636  rabren3dioph  35670  iunrelexp0  36306  dvradcnv2  36707  xpexb  36818  fsumcnf  37352  fprodcncf  37789  iblconstmpt  37842  itgiccshift  37867  itgperiod  37868  itgsbtaddcnst  37869  dirkercncflem2  37976  fourierdlem47  38027  sge0iunmpt  38270  sge0xaddlem2  38286  sge0xadd  38287  hoidmvlelem3  38429  aoprssdm  38714  residfi  39049  usgrnbcnvfv  39449  ewlksfval  39628