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 }

This proof depends on syntax axioms:   {cab 2224   F/_wnfc 2379

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-nfc 2381

This theorem is used by:  abid2f  2418  nfrab1  2732  elabgt  2967  elabgf  2968  nfsbc1d  3068  ss2ab  3316  abn0r  3546  euabsn  3781  iunab  4059  iinab  4074  iotaexab  5356  sniota  5368  nfixp1  7000  modom  7108  hashf1lem2  11286  elabgft1  16806  elabgf2  16808