Theorem nfab1 2907

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

Syntax hints:  {cab 2714  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-nfc 2892

This theorem is referenced by:  nfabd2  2929  eqabf  2935  abid2fOLD  2937  nfrab1  3457  elabgf  3674  nfsbc1d  3806  ss2ab  4062  ab0ALT  4381  euabsn  4726  iunab  5051  iinab  5068  zfrep4  5293  rnep  5937  sniota  6552  opabiotafun  6989  nfixp1  8958  scottexs  9927  scott0s  9928  cp  9931  symgval  19388  ofpreima  32675  algextdeglem6  33763  qqhval2  33983  esum2dlem  34093  sigaclcu2  34121  bnj1366  34843  bnj1321  35041  bnj1384  35046  currysetlem  36946  currysetlem1  36948  bj-reabeq  37028  mptsnunlem  37339  topdifinffinlem  37348  scottabf  44259  compab  44461  ssfiunibd  45321  absnsb  47039  setrec2lem2  49213