Theorem syl6eqel 1553

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 1545	1 |- (ph -> A e. C)

Syntax hints:   -> wi 3   = wceq 954   e. wcel 956

This theorem is referenced by:  syl6eqelr 1554  class2set 2729  moabex 2761  prex 2776  unisn2 2870  onun 3105  relsn 3249  zfrep6 3606  elimdeloprv 3992  ndmoprcl 4036  oesuc 4156  omcl 4161  oecl 4162  nnmcl 4220  nnecl 4221  xpsnen 4421  pw2en 4432  noinfep 4620  rankon 4651  alephon 4845  recclpq 5052  nn0addclt 6075  nn0mulcl 6077  znegclt 6118  elnn0nn 6126  zeot 6154  limsupclt 6470  expcllem 6515  faclbnd4lem3 6895  bccl2t 6917  bcclt 6918  serzcmp0 7001  bcxmas 7022  iserzcmp0 7087  eirrlem4 7341  eirrlem5 7342  acdc3lem 7436  acdc2lem1 7438  acdclem 7444  infpnlem2 7458  sn0top 7597  indistop 7598  iooretop 7609  0blo 8397  nmlno0lem 8398  resslogrn 8692  omlsilem 9182  pjoc1 9202  nonbool 9536  nmlnop0ALT 9858  unopbdt 9878  lnopcon 9901  lnfncon 9928  leoprf2t 9998  pjbdln 10014  pjcmmul1 10067  eloi 10539  aidm 10563  aidmold 10564

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain