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

Theorem nfab 2573
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 2420 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2559 1  |-  F/_ x { y  |  ph }
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1661   {cab 2414   F/_wnfc 2556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-nfc 2558
This theorem is referenced by:  nfaba1  2574  nfun  3565  sbcel12  3745  sbceqg  3746  nfpw  3936  nfpr  3990  nfuni  4168  nfint  4208  intab  4229  nfiun  4270  nfiin  4271  nfiu1  4272  nfii1  4273  nfopab  4432  nfopab1  4433  nfopab2  4434  nfdm  5038  eusvobj2  6242  nfoprab1  6298  nfoprab2  6299  nfoprab3  6300  nfoprab  6301  fun11iun  6711  nfwrecs  6985  nfixp  7496  nfixp1  7497  reclem2pr  9424  nfwrd  12643  mreiincl  15445  lss1d  18129  disjabrex  28138  disjabrexf  28139  esumc  28824  bnj900  29692  bnj1014  29723  bnj1123  29747  bnj1307  29784  bnj1398  29795  bnj1444  29804  bnj1445  29805  bnj1446  29806  bnj1447  29807  bnj1467  29815  bnj1518  29825  bnj1519  29826  dfon2lem3  30382  sdclem1  31979  heibor1  32049  dihglblem5  34778  sbcel12gOLD  36818  ssfiunibd  37424  hoidmvlelem1  38264
  Copyright terms: Public domain W3C validator