Theorem nfab 2286

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

Hypothesis

Ref	Expression
nfab.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfab	⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Proof of Theorem nfab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfab.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nfsab 2131	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2271	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1436  {cab 2125  Ⅎwnfc 2268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-nfc 2270

This theorem is referenced by:  nfaba1  2287  nfrabxy  2611  sbcel12g  3017  sbceqg  3018  nfun  3232  nfpw  3523  nfpr  3573  nfop  3721  nfuni  3742  nfint  3781  intab  3800  nfiunxy  3839  nfiinxy  3840  nfiunya  3841  nfiinya  3842  nfiu1  3843  nfii1  3844  nfopab  3996  nfopab1  3997  nfopab2  3998  repizf2  4086  nfdm  4783  fun11iun  5388  eusvobj2  5760  nfoprab1  5820  nfoprab2  5821  nfoprab3  5822  nfoprab  5823  nfrecs  6204  nffrec  6293  nfixpxy  6611  nfixp1  6612