Theorem syl5eqel 1975

Description: A membership and equality inference.

Hypotheses

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

Assertion

Ref	Expression
syl5eqel	|- (ph -> C e. B)

Proof of Theorem syl5eqel

Step	Hyp	Ref	Expression
1		syl5eqel.2	. . 3 |- C = A
2	1	a1i 8	. 2 |- (ph -> C = A)
3		syl5eqel.1	. 2 |- (ph -> A e. B)
4	2, 3	eqeltrd 1971	1 |- (ph -> C e. B)

Syntax hints:   -> wi 3   = wceq 1298   e. wcel 1300

This theorem is referenced by:  syl5eqelr 1976  csbexg 2548  abssexgOLD 3491  dmresexg 4236  resexgOLD 4251  cofunexg 4501  cofunex2g 4502  f1oabexg 4650  oprabex2g 4949  foprrn 4965  fnoprvrn 4968  mptexg 5012  mpt2exg 5013  iunon 5114  iinon 5115  oelim2 5270  ecexg 5322  pmex 5386  supcl 5669  hartog 5693  rankelpr 5819  rankelop 5820  scott0 5847  htalem 5857  negcl 6525  uzwo3lem2 7430  quoremz 7492  quoremnn0ALT 7493  quoremnn0 7494  intfrac2 7495  intfracq 7496  seq1rn2 7734  discrlem2 7907  discrlem3 7908  ser0cl 8306  ser1cl 8307  ser1cmp2lem 8436  ser1cmp2i 8437  iserzabslem 8438  isumcl 8470  ivthlem7 8549  efcl 8574  efcnlem2 8685  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  infpnlem1 8775  infpnlem2 8776  topopn 8871  fctop 8920  txuni 8935  cldval 8942  ntrfval 8943  clsfval 8944  iscld 8945  topcld 8951  ntrval 8952  clsval 8953  intcld 8956  uncld 8957  elcls3 8987  neifval 8990  neif 8991  neiss2 8992  neival 8993  isnei 8994  lpfval 9018  lpval 9019  islp2 9023  iscn 9034  iscnp 9036  cnco 9045  metxplem1 9103  metxplem2 9104  blfval 9112  blval 9114  blrn 9118  blf 9121  opnfval 9134  isopn 9136  lmfval 9203  caufval 9204  lmbr 9206  iscau 9214  fsumcnlem 9267  bcthlem9 9285  grpinvfval 9350  grpinvval 9351  grpinvf 9364  grpdivfval 9366  gxoprval 9380  grplactfval 9404  issubg 9425  isga 9450  gaid 9454  isvc 9532  isnv 9563  imsmet 9656  ubthlem7 9878  ubthlem10 9881  spwval2 9996  tx1cn 10223  tx2cn 10224  uptx 10226  txcn 10227  homeofval 10234  subspid 10249  subtopmetlem 10255  subtopmet 10256  fillsb 10270  elfg 10284  filrn 10293  sfvlim 10296  limfil 10297  filmapf 10307  isfilmap 10308  elfilmap3 10314  fbfgfmeq 10315  flimff 10317  sflimf 10318  flimfnei 10319  fbaslim 10322  isflimf 10323  holimf 10326  idrval 10374  pjthlem2 10853  pjthlem4 10855  pjoc1i 10897  osumi 11221  nmcopexlem4 11591  nmcfnexlem4 11620  cnlnadjlem3 11639  mdsymlem1 11975  mdsymlem3 11977  bnj547 13273  bnj889 13323  bnj944 13340  bnj969 13351  bnj1136 13435  bnj1177 13445  bnj1410 13520  bnj1462 13546  bnj1489 13554  fseq1cl 13619  seq0cl 13620  ghomgrp 13633  algrf 13739  algcvg 13744  algcvga 13747  algfx 13748  eucalgf 13751  eucalgcvga 13754  axfelem1 14031  axfelem10 14040  altxpsspw 14100  oprabex2gpop 14337  inpws2 14346  fnoprvrn2 14352  isprj2 14506  iscst1 14519  valcurfn1 14552  ppldrels 14568  ubos 14599  supdefa 14605  mxlelt 14607  defge3 14613  inposet 14620  tolat 14631  toplat 14638  unsgrp 14728  gaplc 14731  gapm2 14732  trset 14756  inttop3 14864  mapudiscn 14872  idhme 14879  hmphre 14884  homcardus 14894  qusp 14908  ttcn 14913  conttnf 14944  conttnf2 14945  cnpfillim4 14947  bwt2 14960  topgrpsubcnlem 14981  topgrpsubcn 14982  cntrsetlem 14999  flimfneicn 15037  supbrr 15048  idsubfun 15206  tarone 15232  tartwo 15233  tarorpa 15236  cptarc 15242  carinttar 15279  cartarlim 15282  isline1 15294  isseg1 15304  isseg2 15305  hartogOLD 15384  opncldf1 15402  cncls 15419  subcls 15424  subntr 15425  reconnlem3 15448  locfindsc 15515  ufilss 15567  ufileulem 15572  ufileu 15573  filufint 15574  uffixfr 15575  ufinffr 15578  filcon 15580  ufcondr 15581  flimcls 15588  cnpfillim 15589  fmfnfmlem4 15597  fmfnfm 15598  flimfbas 15601  flimfcnp 15602  sfcls 15604  fclusbas 15610  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomp 15621  fclusff 15623  sfclusf 15624  isfclusf 15625  flfssfcf 15629  uffcfflf 15630  tailf 15633  filnetlem4 15643  filnet 15645  upixp 15729  abrexex2g 15738  firnfi3 15743  supex2g 15761  fisup2g 15768  isumclf 15828  subspopn 15837  subspabs 15840  blssp 15844  cnimass 15888  cnss 15892  ishomeo2 15896  tlmval 15903  txsubsp 15912  sstotbnd 15936  totbndss 15937  totbndbnd 15944  ismtyval 15947  isismty 15948  ismtyres 15954  rrntotbnd 16022  rrnheibor 16023  exidres 16031  exidresid 16032  phtpycolem5 16055  pcohtpylem3 16082  pcorev 16087  stbel 16729  stbval 16731  osumcllem1 17364  osumcllem9 17372  pexmidlem6 17383

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain