Theorem nfab1 2394

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 2228	. 2 |- F/ x y e. { x | ph }
2	1	nfci 2382	1 |- F/_ x { x | ph }

Syntax hints:   {cab 2224   F/_wnfc 2379

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-nfc 2381

This theorem is referenced by:  abid2f  2418  nfrab1  2732  elabgt  2967  elabgf  2968  nfsbc1d  3068  ss2ab  3316  abn0r  3546  euabsn  3777  iunab  4054  iinab  4069  iotaexab  5351  sniota  5363  nfixp1  6990  modom  7098  hashf1lem2  11264  elabgft1  16720  elabgf2  16722