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

Theorem nfab 2575
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 2427 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2561 1  |-  F/_ x { y  |  ph }
Colors of variables: wff set class
Syntax hints:   F/wnf 1553   {cab 2421   F/_wnfc 2558
This theorem is referenced by:  nfaba1  2576  sbcel12g  3258  sbceqg  3259  nfun  3495  nfpw  3802  nfpr  3847  nfuni  4013  nfint  4052  intab  4072  nfiun  4111  nfiin  4112  nfiu1  4113  nfii1  4114  nfopab  4265  nfopab1  4266  nfopab2  4267  nfdm  5103  fun11iun  5687  nfoprab1  6115  nfoprab2  6116  nfoprab3  6117  nfoprab  6118  eusvobj2  6574  nfrecs  6627  nfixp  7073  nfixp1  7074  reclem2pr  8917  nfwrd  11732  mreiincl  13813  lss1d  16031  disjabrex  24016  disjabrexf  24017  esumc  24438  dfon2lem3  25404  nfwrecs  25525  sdclem1  26428  heibor1  26500  bnj900  29227  bnj1014  29258  bnj1123  29282  bnj1307  29319  bnj1398  29330  bnj1444  29339  bnj1445  29340  bnj1446  29341  bnj1447  29342  bnj1467  29350  bnj1518  29360  bnj1519  29361  dihglblem5  32023
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-nfc 2560
  Copyright terms: Public domain W3C validator