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

Theorem nfab 2620
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 2445 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2605 1  |-  F/_ x { y  |  ph }
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1621   {cab 2439   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-nfc 2604
This theorem is referenced by:  nfaba1  2621  nfun  3646  sbcel12  3822  sbceqg  3823  nfpw  4011  nfpr  4063  nfuni  4241  nfint  4281  intab  4302  nfiun  4343  nfiin  4344  nfiu1  4345  nfii1  4346  nfopab  4504  nfopab1  4505  nfopab2  4506  nfdm  5233  eusvobj2  6263  nfoprab1  6319  nfoprab2  6320  nfoprab3  6321  nfoprab  6322  fun11iun  6733  nfrecs  7036  nfixp  7481  nfixp1  7482  reclem2pr  9415  nfwrd  12557  mreiincl  15085  lss1d  17804  disjabrex  27653  disjabrexf  27654  esumc  28280  dfon2lem3  29457  nfwrecs  29578  sdclem1  30476  heibor1  30546  ssfiunibd  31748  sbcel12gOLD  33705  bnj900  34388  bnj1014  34419  bnj1123  34443  bnj1307  34480  bnj1398  34491  bnj1444  34500  bnj1445  34501  bnj1446  34502  bnj1447  34503  bnj1467  34511  bnj1518  34521  bnj1519  34522  dihglblem5  37422
  Copyright terms: Public domain W3C validator