Theorem syl5eqel 1550

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 1546	1 |- (ph -> C e. B)

Syntax hints:   -> wi 3   = wceq 955   e. wcel 957

This theorem is referenced by:  syl5eqelr 1551  csbexg 2005  abssexg 2743  dmresexg 3378  resexg 3390  cofunexg 3576  cofunex2g 3577  f1oabexg 3695  iunon 3904  iinon 3905  oprabex2g 4015  foprrn 4030  fnoprvalrn 4033  oelim2 4215  ecexg 4258  pmex 4320  supcl 4562  rankelpr 4691  rankelop 4692  scott0 4700  htalem 4710  negclt 5351  uzwo3lem2 6175  seq1rn2 6271  discrlem2 6602  discrlem3 6603  ser0clt 6999  ser1clt 7000  ser1cmp2lem 7129  ser1cmp2 7130  iserzabslem 7131  isumclt 7161  ivthlem7 7239  ivthlem7OLD 7248  efclt 7271  efcnlem2 7377  acdc3lem 7445  acdc2lem2 7448  acdc5lem2 7451  acdclem 7453  infpnlem1 7466  infpnlem2 7467  topopn 7562  indistop 7608  cldval 7626  ntrfval 7627  clsfval 7628  iscld 7629  topcld 7635  ntrval 7636  clsval 7637  intcld 7640  uncld 7641  elcls3 7671  neifval 7674  neif 7675  neiss2 7676  neival 7677  isnei 7678  lpfval 7702  lpval 7703  islp2 7707  iscn 7718  iscnp 7720  cnco 7728  metxplem1 7788  metxplem2 7789  blfval 7797  blval 7799  blrn 7803  blf 7806  opnfval 7819  isopn 7821  lmfval 7887  caufval 7888  lmbr 7890  iscau 7898  fsumcnlem 7951  bcthlem9 7969  grpidval 8020  grpinvfval 8028  grpinvval 8029  grpinvf 8041  grpdivfval 8043  grplactfval 8059  issubg 8080  isvc 8164  isnv 8195  imsmet 8288  ubthlem7 8494  ubthlem10 8497  spwval2 8610  pjthlem2 9175  pjthlem4 9177  pjoc1 9219  osum 9543  nmcopexlem4 9910  nmcfnexlem4 9939  cnlnadjlem3 9958  mdsymlem1 10286  mdsymlem3 10288  ghomgrp 10346  inpws2 10410  fnoprvalrn2 10424  mapudiscn 10458  homeofval 10462  idhme 10468  hmphre 10476  qusp 10489  sfvlim 10522

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-cleq 1468  df-clel 1471

Copyright terms: Public domain