Theorem nfab1 2766

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

Syntax hints:   {cab 2608   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-nfc 2753

This theorem is referenced by:  nfabd2  2784  abid2f  2791  nfrab1  3122  elabgt  3347  elabgf  3348  nfsbc1d  3453  ss2ab  3670  ab0  3951  abn0  3954  euabsn  4261  iunab  4566  iinab  4581  zfrep4  4779  sniota  5878  opabiotafun  6259  nfixp1  7928  scottexs  8750  scott0s  8751  cp  8754  ofpreima  29465  qqhval2  30026  esum2dlem  30154  sigaclcu2  30183  bnj1366  30900  bnj1321  31095  bnj1384  31100  mptsnunlem  33185  topdifinffinlem  33195  compab  38645  ssfiunibd  39523  setrec2lem2  42441