Theorem nfab1 2376

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.

Step	Hyp	Ref	Expression
1		nfsab1 2221	. 2 |- F/ x y e. { x | ph }
2	1	nfci 2364	1 |- F/_ x { x | ph }

Syntax hints:   {cab 2217   F/_wnfc 2361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-nfc 2363

This theorem is referenced by:  abid2f  2400  nfrab1  2713  elabgt  2947  elabgf  2948  nfsbc1d  3048  ss2ab  3295  abn0r  3519  euabsn  3741  iunab  4017  iinab  4032  iotaexab  5305  sniota  5317  nfixp1  6886  modom  6993  elabgft1  16374  elabgf2  16376