Theorem nfab1 2981

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 2810	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
2	1	nfci 2966	1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Syntax hints:  {cab 2801  Ⅎwnfc 2963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-nfc 2965

This theorem is referenced by:  nfabd2  3004  nfabd2OLD  3005  abid2f  3014  abeq2f  3015  nfrab1  3386  elabgt  3665  elabgf  3666  elabg  3668  nfsbc1d  3792  ss2ab  4041  ab0  4335  abn0  4338  euabsn  4664  iunab  4977  iinab  4992  zfrep4  5202  rnep  5799  sniota  6348  opabiotafun  6746  nfixp1  8484  scottexs  9318  scott0s  9319  cp  9322  symgval  18499  ofpreima  30412  qqhval2  31225  esum2dlem  31353  sigaclcu2  31381  bnj1366  32103  bnj1321  32301  bnj1384  32306  currysetlem  34258  currysetlem1  34260  bj-reabeq  34341  mptsnunlem  34621  topdifinffinlem  34630  scottabf  40583  compab  40781  ssfiunibd  41583  absnsb  43269  setrec2lem2  44804