Theorem syl6eqel 1979

Description: A membership and equality inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl6eqel

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

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

This theorem is referenced by:  syl6eqelr 1980  class2set 3471  snex 3492  moabex 3513  prex 3526  onun2i 3785  unisn2 3799  relsn 4087  zfrep6 4545  elimdeloprv 4930  ndmoprcl 4977  iotaex 5099  oesuc 5211  omcl 5216  omclOLD 5217  oecl 5218  oeclOLD 5219  nnmcl 5283  nnmclOLD 5284  nnecl 5285  nneclOLD 5286  xpsnen 5494  pw2en 5505  ac6sfilem3 5508  unifi 5648  noinfep 5747  rankon 5782  alephon 5876  recclpq 6224  nn0addcl 7329  nn0mulcli 7331  znegcl 7372  elnn0nn 7380  zeo 7411  limsupcl 7773  expcllem 7818  faclbnd4lem3 8202  bccl2 8223  bccl 8224  serzcmp0 8315  bcxmas 8336  iserzcmp0 8403  eirrlem4 8654  eirrlem5 8655  acdc3lem 8754  acdc2lem1 8757  acdclem 8763  infpnlem2 8776  sn0top 8917  indistop 8918  iooretop 8929  vacnlem4 9670  0blo 9792  nmlno0lem 9793  resslogrn 10107  fixp 10180  stoig 10251  omlsilem 10877  pjoc1i 10897  nonbooli 11231  nmlnop0iALT 11557  unopbd 11577  lnopconi 11600  lnfnconi 11627  leoprf2 11698  opsqrlem5 11715  pjbdlni 11720  pjcmmul1i 11774  eqreznegel 13654  bdayelon 14017  eloi 14400  fixpc 14418  rngunval2 14774  subempcomp 14954  subsincomp 14956  singempcon 14965  empcon 14966  aidm2 15097  tmpts 15257  topmtcl 15525  ufinffr 15578  prfOLD 15680  fzfi 15786  heiborlem18 15972  bfplem3 16000  elpi1 16089

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