Theorem nfab1 2951

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

Syntax hints:  {cab 2775  Ⅎwnfc 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-10 2112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-nfc 2935

This theorem is referenced by:  nfabd2  2970  nfabd2OLD  2971  abid2f  2980  abeq2f  2981  nfrab1  3344  elabgt  3601  elabgf  3602  elabg  3604  nfsbc1d  3724  ss2ab  3960  ab0  4253  abn0  4256  euabsn  4569  iunab  4874  iinab  4889  zfrep4  5091  sniota  6216  opabiotafun  6611  nfixp1  8330  scottexs  9162  scott0s  9163  cp  9166  ofpreima  30100  qqhval2  30840  esum2dlem  30968  sigaclcu2  30996  bnj1366  31718  bnj1321  31913  bnj1384  31918  currysetlem  33827  currysetlem1  33829  mptsnunlem  34150  topdifinffinlem  34159  scottabf  40073  compab  40313  ssfiunibd  41117  absnsb  42778  setrec2lem2  44277