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

Theorem nfab 2633
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 2458 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2618 1  |-  F/_ x { y  |  ph }
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1599   {cab 2452   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-nfc 2617
This theorem is referenced by:  nfaba1  2634  nfun  3660  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  nfpw  4022  nfpr  4074  nfuni  4251  nfint  4292  intab  4312  nfiun  4353  nfiin  4354  nfiu1  4355  nfii1  4356  nfopab  4512  nfopab1  4513  nfopab2  4514  nfdm  5242  eusvobj2  6275  nfoprab1  6328  nfoprab2  6329  nfoprab3  6330  nfoprab  6331  fun11iun  6741  nfrecs  7041  nfixp  7485  nfixp1  7486  reclem2pr  9422  nfwrd  12531  mreiincl  14847  lss1d  17392  disjabrex  27116  disjabrexf  27117  esumc  27702  dfon2lem3  28794  nfwrecs  28915  sdclem1  29839  heibor1  29909  upbdrech  31082  ssfiunibd  31086  bnj900  33066  bnj1014  33097  bnj1123  33121  bnj1307  33158  bnj1398  33169  bnj1444  33178  bnj1445  33179  bnj1446  33180  bnj1447  33181  bnj1467  33189  bnj1518  33199  bnj1519  33200  dihglblem5  36095
  Copyright terms: Public domain W3C validator