New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfab Unicode 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
Assertion
Ref Expression
nfab

Proof of Theorem nfab
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3
21nfsab 2345 . 2
32nfci 2479 1
 Colors of variables: wff setvar class Syntax hints:  wnf 1544  cab 2339  wnfc 2476 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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