Theorem nfab 2313

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

Syntax hints:  Ⅎwnf 1448  {cab 2151  Ⅎwnfc 2295

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-nfc 2297

This theorem is referenced by:  nfaba1  2314  nfrabxy  2646  sbcel12g  3060  sbceqg  3061  nfun  3278  nfpw  3572  nfpr  3626  nfop  3774  nfuni  3795  nfint  3834  intab  3853  nfiunxy  3892  nfiinxy  3893  nfiunya  3894  nfiinya  3895  nfiu1  3896  nfii1  3897  nfopab  4050  nfopab1  4051  nfopab2  4052  repizf2  4141  nfdm  4848  fun11iun  5453  eusvobj2  5828  nfoprab1  5891  nfoprab2  5892  nfoprab3  5893  nfoprab  5894  nfrecs  6275  nffrec  6364  nfixpxy  6683  nfixp1  6684