Theorem nfab 2494

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 2480	1 ⊢ Ⅎx{y ∣ φ}

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2479

This theorem is referenced by:  nfaba1  2495  sbcel12g  3152  sbceqg  3153  nfnin  3229  nfpw  3734  nfpr  3774  nfuni  3898  nfint  3937  intab  3957  nfiun  3996  nfiin  3997  nfiu1  3998  nfii1  3999  nfop  4605  nfopab  4628  nfopab1  4629  nfopab2  4630  nfima  4954  fun11iun  5306  nfoprab1  5547  nfoprab2  5548  nfoprab3  5549  nfoprab  5550