Theorem syl5eqelr 2706

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 2631	. 2 |- A = B
3		syl5eqelr.2	. 2 |- ( ph -> B e. C )
4	2, 3	syl5eqel 2705	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  3eltr3g  2717  dmrnssfld  5384  oprssdm  6815  offval  6904  pwexr  6974  cnvexg  7112  resfunexgALT  7129  abrexexg  7140  abrexex2g  7144  opabex3d  7145  suppssov1  7327  suppssfv  7331  ralxpmap  7907  residfi  8247  imafi  8259  abrexfi  8266  ssfii  8325  wdomima2g  8491  unxpwdom2  8493  tskwe  8776  ac10ct  8857  fin23lem28  9162  fin23lem30  9164  axcclem  9279  distrlem4pr  9848  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  o1res  14291  exprmfct  15416  infpnlem1  15614  4sqlem13  15661  0ram  15724  ressval3d  15937  ismred2  16263  mreexexlem2d  16305  mreexexlem4d  16307  acsfn1c  16323  acsfn2  16324  ssclem  16479  submacs  17365  efgrcl  18128  dprd2da  18441  srgbinom  18545  irredlmul  18708  lidlrsppropd  19230  issubassa  19324  ply1crng  19568  ply1ring  19618  ply1lmod  19622  chrcl  19874  css1  20034  oftpos  20258  tposmap  20263  0opn  20709  fctop2  20809  difopn  20838  tgrest  20963  ordtbas2  20995  ordtopn3  21000  ordtcld3  21003  t1ficld  21131  resthauslem  21167  kgentopon  21341  txbasex  21369  txcnpi  21411  txdis1cn  21438  pthaus  21441  txkgen  21455  cnmptid  21464  cnmptc  21465  cnmpt1st  21471  cnmpt2nd  21472  cnmpt2c  21473  cnmptkc  21482  txconn  21492  hmeoima  21568  hmeocld  21570  xkohmeo  21618  filufint  21724  fin1aufil  21736  flftg  21800  ptcmplem2  21857  tmdmulg  21896  tmdgsum2  21900  symgtgp  21905  submtmd  21908  ghmcnp  21918  qustgpopn  21923  qustgplem  21924  ust0  22023  nrginvrcn  22496  fsumcn  22673  fsum2cn  22674  expcn  22675  cnheibor  22754  evth2  22759  csscld  23048  clsocv  23049  ovoliun2  23274  volfiniun  23315  dyadmbl  23368  mbfeqalem  23409  mbfss  23413  ismbf3d  23421  mbfadd  23428  i1f0rn  23449  mbfmul  23493  itg2seq  23509  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itgreval  23563  itgge0  23577  itgss3  23581  iblconst  23584  itgconst  23585  ibladdlem  23586  itgfsum  23593  iblabslem  23594  itgabs  23601  mvth  23755  lhop1lem  23776  dvfsumle  23784  dvfsumlem2  23790  ftc1lem4  23802  itgparts  23810  itgsubstlem  23811  itgsubst  23812  plydivlem1  24048  aannenlem1  24083  taylply2  24122  itgulm  24162  cxpcn  24486  resqrtcn  24490  basellem1  24807  mulogsumlem  25220  mulog2sumlem2  25224  selberg2lem  25239  pntrsumo1  25254  usgrnbcnvfv  26267  ewlksfval  26497  crctcshwlkn0  26713  numclwwlk3lem  27241  pjssmii  28540  abrexexd  29347  ogrpaddltrbid  29721  lmatfval  29880  pl1cn  30001  esumcvg  30148  esumcvgsum  30150  sigaval  30173  sigaclfu2  30184  sigapildsys  30225  ldgenpisys  30229  measinb2  30286  braew  30305  unelcarsg  30374  carsgclctunlem2  30381  sibfof  30402  sitgclg  30404  orrvcoel  30527  orrvccel  30528  fsum2dsub  30685  subfaclefac  31158  cvmsss2  31256  cvmopnlem  31260  mpstrcl  31438  elmpps  31470  hmeoclda  32328  bj-1uplex  32996  bj-2uplex  33010  bj-diagval  33090  icoreclin  33205  broucube  33443  mblfinlem1  33446  cnambfre  33458  ibladdnclem  33466  iblabsnclem  33473  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc2nc  33494  areacirc  33505  zrdivrng  33752  dalemrot  34943  dalem10  34959  arglem1N  35477  cdlemk36  36201  mzpconstmpt  37303  mzpresrename  37313  diophrex  37339  0dioph  37342  anrabdioph  37344  orrabdioph  37345  rabren3dioph  37379  iunrelexp0  37994  dvradcnv2  38546  xpexb  38658  fsumcnf  39180  uzublem  39657  fprodcncf  40114  iblconstmpt  40171  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  dirkercncflem2  40321  fourierdlem47  40370  saluni  40544  sge0iunmpt  40635  sge0xaddlem2  40651  sge0xadd  40652  hoidmvlelem3  40811  ctvonmbl  40903  vonct  40907  smfaddlem2  40972  smfmullem4  41001  aoprssdm  41282