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  3074  sbceqg  3075  nfun  3293  nfpw  3590  nfpr  3644  nfop  3796  nfuni  3817  nfint  3856  intab  3875  nfiunxy  3914  nfiinxy  3915  nfiunya  3916  nfiinya  3917  nfiu1  3918  nfii1  3919  nfopab  4073  nfopab1  4074  nfopab2  4075  repizf2  4164  nfdm  4873  fun11iun  5484  eusvobj2  5864  nfoprab1  5927  nfoprab2  5928  nfoprab3  5929  nfoprab  5930  nfrecs  6311  nffrec  6400  nfixpxy  6720  nfixp1  6721