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

Theorem nfab 2423
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 2275 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2409 1  |-  F/_ x { y  |  ph }
Colors of variables: wff set class
Syntax hints:   F/wnf 1531   {cab 2269   F/_wnfc 2406
This theorem is referenced by:  nfaba1  2424  sbcel12g  3096  sbceqg  3097  nfun  3331  nfpw  3636  nfpr  3680  nfuni  3833  nfint  3872  intab  3892  nfiun  3931  nfiin  3932  nfiu1  3933  nfii1  3934  nfopab  4084  nfopab1  4085  nfopab2  4086  nfdm  4920  fun11iun  5493  nfoprab1  5897  nfoprab2  5898  nfoprab3  5899  nfoprab  5900  eusvobj2  6337  nfrecs  6390  nfixp  6835  nfixp1  6836  axdclem  8146  reclem2pr  8672  nfwrd  11426  mreiincl  13498  lss1d  15720  dfon2lem3  23552  nfprod1  24722  nfprod  24723  intopcoaconb  24952  sdclem1  25865  heibor1  25946  bnj900  28334  bnj1014  28365  bnj1123  28389  bnj1307  28426  bnj1398  28437  bnj1444  28446  bnj1445  28447  bnj1446  28448  bnj1447  28449  bnj1467  28457  bnj1518  28467  bnj1519  28468  dihglblem5  30861
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-nfc 2408
  Copyright terms: Public domain W3C validator