Theorem syl5eqelr 2693

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

Hypotheses

Ref	Expression
syl5eqelr.1	⊢ 𝐵 = 𝐴
syl5eqelr.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
syl5eqelr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl5eqelr

Step	Hyp	Ref	Expression
1		syl5eqelr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2619	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqelr.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	syl5eqel 2692	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  3eltr3g  2704  dmrnssfld  5305  oprssdm  6713  offval  6802  cnvexg  7005  resfunexgALT  7022  abrexexg  7034  abrexex2g  7036  opabex3d  7037  suppssov1  7214  suppssfv  7218  ralxpmap  7793  imafi  8142  abrexfi  8149  ssfii  8208  wdomima2g  8374  unxpwdom2  8376  tskwe  8659  ac10ct  8740  fin23lem28  9045  fin23lem30  9047  axcclem  9162  distrlem4pr  9727  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  o1res  14139  exprmfct  15254  infpnlem1  15452  4sqlem13  15499  0ram  15562  ressval3d  15764  ismred2  16086  mreexexlem2d  16128  mreexexlem4d  16130  acsfn1c  16146  acsfn2  16147  ssclem  16302  submacs  17188  efgrcl  17951  dprd2da  18264  srgbinom  18368  irredlmul  18531  lidlrsppropd  19051  issubassa  19145  ply1crng  19389  ply1ring  19439  ply1lmod  19443  chrcl  19693  css1  19853  oftpos  20077  tposmap  20082  0opn  20534  fctop2  20619  difopn  20648  tgrest  20773  ordtbas2  20805  ordtopn3  20810  ordtcld3  20813  t1ficld  20941  resthauslem  20977  kgentopon  21151  txbasex  21179  txcnpi  21221  txdis1cn  21248  pthaus  21251  txkgen  21265  cnmptid  21274  cnmptc  21275  cnmpt1st  21281  cnmpt2nd  21282  cnmpt2c  21283  cnmptkc  21292  txcon  21302  hmeoima  21378  hmeocld  21380  xkohmeo  21428  filufint  21534  fin1aufil  21546  flftg  21610  ptcmplem2  21667  tmdmulg  21706  tmdgsum2  21710  symgtgp  21715  submtmd  21718  ghmcnp  21728  qustgpopn  21733  qustgplem  21734  ust0  21833  nrginvrcn  22306  fsumcn  22481  fsum2cn  22482  expcn  22483  cnheibor  22562  evth2  22567  csscld  22856  clsocv  22857  ovoliun2  23081  volfiniun  23122  dyadmbl  23174  mbfeqalem  23215  mbfss  23219  ismbf3d  23227  mbfadd  23234  i1f0rn  23255  mbfmul  23299  itg2seq  23315  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itgreval  23369  itgge0  23383  itgss3  23387  iblconst  23390  itgconst  23391  ibladdlem  23392  itgfsum  23399  iblabslem  23400  itgabs  23407  mvth  23559  lhop1lem  23580  dvfsumle  23588  dvfsumlem2  23594  ftc1lem4  23606  itgparts  23614  itgsubstlem  23615  itgsubst  23616  plydivlem1  23852  aannenlem1  23887  taylply2  23926  itgulm  23966  cxpcn  24286  resqrtcn  24290  basellem1  24607  mulogsumlem  25020  mulog2sumlem2  25024  selberg2lem  25039  pntrsumo1  25054  uhgrstrrepelem  25744  nbgracnvfv  25969  pjssmii  27924  abrexexd  28731  ogrpaddltrbid  29052  lmatfval  29208  pl1cn  29329  esumcvg  29475  esumcvgsum  29477  sigaval  29500  sigaclfu2  29511  sigapildsys  29552  ldgenpisys  29556  measinb2  29613  braew  29632  unelcarsg  29701  carsgclctunlem2  29708  sibfof  29729  sitgclg  29731  orrvcoel  29854  orrvccel  29855  subfaclefac  30412  cvmsss2  30510  cvmopnlem  30514  mpstrcl  30692  elmpps  30724  hmeoclda  31498  bj-1uplex  32189  bj-2uplex  32203  bj-diagval  32267  icoreclin  32381  broucube  32613  mblfinlem1  32616  cnambfre  32628  ibladdnclem  32636  iblabsnclem  32643  itgabsnc  32649  ftc1cnnclem  32653  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc2nc  32664  areacirc  32675  zrdivrng  32922  dalemrot  33961  dalem10  33977  arglem1N  34495  cdlemk36  35219  mzpconstmpt  36321  mzpresrename  36331  diophrex  36357  0dioph  36360  anrabdioph  36362  orrabdioph  36363  rabren3dioph  36397  iunrelexp0  37013  dvradcnv2  37568  xpexb  37679  fsumcnf  38203  fprodcncf  38787  iblconstmpt  38847  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  dirkercncflem2  38997  fourierdlem47  39046  sge0iunmpt  39311  sge0xaddlem2  39327  sge0xadd  39328  hoidmvlelem3  39487  ctvonmbl  39580  vonct  39584  smfaddlem2  39650  smfmullem4  39679  aoprssdm  39931  residfi  40340  usgrnbcnvfv  40593  ewlksfval  40803  crctcsh1wlkn0  41024  av-numclwwlk3lem  41538