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

Theorem nfab1 2571
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfab1  |-  F/_ x { x  |  ph }

Proof of Theorem nfab1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfsab1 2418 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2559 1  |-  F/_ x { x  |  ph }
Colors of variables: wff setvar class
Syntax hints:   {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-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:  nfabd2  2588  abid2f  2595  nfrab1  2948  elabgt  3157  elabgf  3158  nfsbc1d  3260  ss2ab  3472  abn0  3724  euabsn  4015  iunab  4288  iinab  4303  zfrep4  4487  sniota  5535  opabiotafun  5886  nfixp1  7497  scottexs  8310  scott0s  8311  cp  8314  ofpreima  28214  qqhval2  28738  esum2dlem  28865  sigaclcu2  28894  bnj1366  29593  bnj1321  29788  bnj1384  29793  mptsnunlem  31647  topdifinffinlem  31657  compab  36707  ssfiunibd  37424
  Copyright terms: Public domain W3C validator