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

Theorem nfab 2436
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 2288 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2422 1  |-  F/_ x { y  |  ph }
Colors of variables: wff set class
Syntax hints:   F/wnf 1534   {cab 2282   F/_wnfc 2419
This theorem is referenced by:  nfaba1  2437  sbcel12g  3109  sbceqg  3110  nfun  3344  nfpw  3649  nfpr  3693  nfuni  3849  nfint  3888  intab  3908  nfiun  3947  nfiin  3948  nfiu1  3949  nfii1  3950  nfopab  4100  nfopab1  4101  nfopab2  4102  nfdm  4936  fun11iun  5509  nfoprab1  5913  nfoprab2  5914  nfoprab3  5915  nfoprab  5916  eusvobj2  6353  nfrecs  6406  nfixp  6851  nfixp1  6852  axdclem  8162  reclem2pr  8688  nfwrd  11442  mreiincl  13514  lss1d  15736  disjabrex  23374  disjabrexf  23375  esumc  23445  dfon2lem3  24212  nfprod1  25413  nfprod  25414  intopcoaconb  25643  sdclem1  26556  heibor1  26637  bnj900  29277  bnj1014  29308  bnj1123  29332  bnj1307  29369  bnj1398  29380  bnj1444  29389  bnj1445  29390  bnj1446  29391  bnj1447  29392  bnj1467  29400  bnj1518  29410  bnj1519  29411  dihglblem5  32110
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-nfc 2421
  Copyright terms: Public domain W3C validator