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  2657  sbcel12g  3072  sbceqg  3073  nfun  3291  nfpw  3588  nfpr  3642  nfop  3794  nfuni  3815  nfint  3854  intab  3873  nfiunxy  3912  nfiinxy  3913  nfiunya  3914  nfiinya  3915  nfiu1  3916  nfii1  3917  nfopab  4071  nfopab1  4072  nfopab2  4073  repizf2  4162  nfdm  4871  fun11iun  5482  eusvobj2  5860  nfoprab1  5923  nfoprab2  5924  nfoprab3  5925  nfoprab  5926  nfrecs  6307  nffrec  6396  nfixpxy  6716  nfixp1  6717