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

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

Proof of Theorem nfab
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3  |-  F/ x ph
21nfsab 2380 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2514 1  |-  F/_ x { y  |  ph }
Colors of variables: wff set class
Syntax hints:   F/wnf 1550   {cab 2374   F/_wnfc 2511
This theorem is referenced by:  nfaba1  2529  sbcel12g  3210  sbceqg  3211  nfun  3447  nfpw  3754  nfpr  3799  nfuni  3964  nfint  4003  intab  4023  nfiun  4062  nfiin  4063  nfiu1  4064  nfii1  4065  nfopab  4215  nfopab1  4216  nfopab2  4217  nfdm  5052  fun11iun  5636  nfoprab1  6063  nfoprab2  6064  nfoprab3  6065  nfoprab  6066  eusvobj2  6519  nfrecs  6572  nfixp  7018  nfixp1  7019  reclem2pr  8859  nfwrd  11668  mreiincl  13749  lss1d  15967  disjabrex  23869  disjabrexf  23870  esumc  24243  dfon2lem3  25166  sdclem1  26139  heibor1  26211  bnj900  28639  bnj1014  28670  bnj1123  28694  bnj1307  28731  bnj1398  28742  bnj1444  28751  bnj1445  28752  bnj1446  28753  bnj1447  28754  bnj1467  28762  bnj1518  28772  bnj1519  28773  dihglblem5  31414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-nfc 2513
  Copyright terms: Public domain W3C validator