Theorem nfab 2493

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfab.1	⊢ Ⅎxφ

Assertion

Ref	Expression
nfab	⊢ Ⅎx{y ∣ φ}

Proof of Theorem nfab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfab.1	. . 3 ⊢ Ⅎxφ
2	1	nfsab 2345	. 2 ⊢ Ⅎx z ∈ {y ∣ φ}
3	2	nfci 2479	1 ⊢ Ⅎx{y ∣ φ}

Syntax hints:  Ⅎwnf 1544  {cab 2339  Ⅎwnfc 2476

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-nfc 2478

This theorem is referenced by:  nfaba1  2494  sbcel12g  3151  sbceqg  3152  nfnin  3228  nfpw  3733  nfpr  3773  nfuni  3897  nfint  3936  intab  3956  nfiun  3995  nfiin  3996  nfiu1  3997  nfii1  3998  nfop  4604  nfopab  4627  nfopab1  4628  nfopab2  4629  nfima  4953  fun11iun  5305  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548  nfoprab  5549