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

Theorem nfab1 2631
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 2456 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2618 1  |-  F/_ x { x  |  ph }
Colors of variables: wff setvar class
Syntax hints:   {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-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:  nfabd2  2650  abid2f  2658  abid2fOLD  2659  nfrab1  3042  elabgt  3247  elabgf  3248  nfsbc1d  3349  ss2ab  3568  abn0  3804  euabsn  4099  iunab  4371  iinab  4386  zfrep4  4566  sniota  5576  opabiotafun  5926  nfixp1  7486  scottexs  8301  scott0s  8302  cp  8305  ofpreima  27179  qqhval2  27599  sigaclcu2  27760  compab  30928  ssfiunibd  31086  bnj1366  32967  bnj1321  33162  bnj1384  33167
  Copyright terms: Public domain W3C validator