Theorem nfab1 2894

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

Syntax hints:  {cab 2708  Ⅎwnfc 2877

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 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-nfc 2879

This theorem is referenced by:  nfabd2  2916  eqabf  2922  abid2fOLD  2924  nfrab1  3429  elabgf  3644  nfsbc1d  3774  ss2ab  4028  ab0ALT  4347  euabsn  4693  iunab  5018  iinab  5035  zfrep4  5251  rnep  5893  sniota  6505  opabiotafun  6944  nfixp1  8894  scottexs  9847  scott0s  9848  cp  9851  symgval  19308  ofpreima  32596  algextdeglem6  33719  qqhval2  33979  esum2dlem  34089  sigaclcu2  34117  bnj1366  34826  bnj1321  35024  bnj1384  35029  currysetlem  36940  currysetlem1  36942  bj-reabeq  37022  mptsnunlem  37333  topdifinffinlem  37342  scottabf  44236  compab  44438  permaxrep  45003  ssfiunibd  45314  absnsb  47032  setrec2lem2  49687