MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfab Unicode version

Theorem nfab 2623
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 2448 . 2
32nfci 2608 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1616  {cab 2442  F/_wnfc 2605
This theorem is referenced by:  nfaba1  2624  nfun  3659  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  nfpw  4024  nfpr  4076  nfuni  4255  nfint  4296  intab  4317  nfiun  4358  nfiin  4359  nfiu1  4360  nfii1  4361  nfopab  4517  nfopab1  4518  nfopab2  4519  nfdm  5249  eusvobj2  6289  nfoprab1  6346  nfoprab2  6347  nfoprab3  6348  nfoprab  6349  fun11iun  6760  nfrecs  7063  nfixp  7508  nfixp1  7509  reclem2pr  9447  nfwrd  12569  mreiincl  14993  lss1d  17609  disjabrex  27443  disjabrexf  27444  esumc  28062  dfon2lem3  29217  nfwrecs  29338  sdclem1  30236  heibor1  30306  ssfiunibd  31509  bnj900  33987  bnj1014  34018  bnj1123  34042  bnj1307  34079  bnj1398  34090  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1447  34102  bnj1467  34110  bnj1518  34120  bnj1519  34121  dihglblem5  37025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-nfc 2607
  Copyright terms: Public domain W3C validator