Theorem nfab1 2897

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

Syntax hints:  {cab 2701  Ⅎwnfc 2875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-nfc 2877

This theorem is referenced by:  nfabd2  2921  eqabf  2927  abid2fOLD  2929  nfrab1  3443  elabgtOLD  3655  elabgf  3656  elabgOLD  3659  nfsbc1d  3787  ss2ab  4048  ab0ALT  4368  abn0OLD  4373  euabsn  4722  iunab  5044  iinab  5061  zfrep4  5286  rnep  5916  sniota  6524  opabiotafun  6962  nfixp1  8907  scottexs  9877  scott0s  9878  cp  9881  symgval  19273  ofpreima  32314  algextdeglem6  33224  qqhval2  33417  esum2dlem  33545  sigaclcu2  33573  bnj1366  34295  bnj1321  34493  bnj1384  34498  currysetlem  36282  currysetlem1  36284  bj-reabeq  36364  mptsnunlem  36675  topdifinffinlem  36684  scottabf  43454  compab  43656  ssfiunibd  44470  absnsb  46188  setrec2lem2  47893