Theorem nfab1 2905

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfab1	⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Proof of Theorem nfab1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfsab1 2717	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
2	1	nfci 2886	1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Syntax hints:  {cab 2709  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-nfc 2885

This theorem is referenced by:  nfabd2  2929  eqabf  2935  abid2fOLD  2937  nfrab1  3451  elabgtOLD  3663  elabgf  3664  elabgOLD  3667  nfsbc1d  3795  ss2ab  4056  ab0ALT  4376  abn0OLD  4381  euabsn  4730  iunab  5054  iinab  5071  zfrep4  5296  rnep  5926  sniota  6534  opabiotafun  6972  nfixp1  8911  scottexs  9881  scott0s  9882  cp  9885  symgval  19235  ofpreima  31885  qqhval2  32957  esum2dlem  33085  sigaclcu2  33113  bnj1366  33835  bnj1321  34033  bnj1384  34038  currysetlem  35821  currysetlem1  35823  bj-reabeq  35903  mptsnunlem  36214  topdifinffinlem  36223  scottabf  42989  compab  43191  ssfiunibd  44009  absnsb  45727  setrec2lem2  47729