Theorem nfab 2324

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 2169	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2309	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1460  {cab 2163  Ⅎwnfc 2306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-nfc 2308

This theorem is referenced by:  nfaba1  2325  nfrabxy  2658  sbcel12g  3073  sbceqg  3074  nfun  3292  nfpw  3589  nfpr  3643  nfop  3795  nfuni  3816  nfint  3855  intab  3874  nfiunxy  3913  nfiinxy  3914  nfiunya  3915  nfiinya  3916  nfiu1  3917  nfii1  3918  nfopab  4072  nfopab1  4073  nfopab2  4074  repizf2  4163  nfdm  4872  fun11iun  5483  eusvobj2  5861  nfoprab1  5924  nfoprab2  5925  nfoprab3  5926  nfoprab  5927  nfrecs  6308  nffrec  6397  nfixpxy  6717  nfixp1  6718