NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl5eqelr GIF version

Theorem syl5eqelr 2438
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqelr.1 B = A
syl5eqelr.2 (φB C)
Assertion
Ref Expression
syl5eqelr (φA C)

Proof of Theorem syl5eqelr
StepHypRef Expression
1 syl5eqelr.1 . . 3 B = A
21eqcomi 2357 . 2 A = B
3 syl5eqelr.2 . 2 (φB C)
42, 3syl5eqel 2437 1 (φA C)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1642   wcel 1710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349
This theorem is referenced by:  xpkexg  4288  pw1exb  4326  nncaddccl  4419  0cminle  4461  vfinspsslem1  4550  opexb  4603  cnvexb  5103  epprc  5827  frds  5935  ovmuc  6130  ovcelem1  6171  ce2t  6235  addccan2nclem2  6264  fnfreclem1  6317  elscan  6330
  Copyright terms: Public domain W3C validator