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

Theorem nfab 2493
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfab.1 xφ
Assertion
Ref Expression
nfab x{y φ}

Proof of Theorem nfab
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3 xφ
21nfsab 2345 . 2 x z {y φ}
32nfci 2479 1 x{y φ}
Colors of variables: wff setvar class
Syntax hints:  wnf 1544  {cab 2339  wnfc 2476
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-6 1729  ax-7 1734  ax-11 1746  ax-12 1925
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-nfc 2478
This theorem is referenced by:  nfaba1  2494  sbcel12g  3151  sbceqg  3152  nfnin  3228  nfpw  3733  nfpr  3773  nfuni  3897  nfint  3936  intab  3956  nfiun  3995  nfiin  3996  nfiu1  3997  nfii1  3998  nfop  4604  nfopab  4627  nfopab1  4628  nfopab2  4629  nfima  4953  fun11iun  5305  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548  nfoprab  5549
  Copyright terms: Public domain W3C validator