Theorem nfab 2317

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

Syntax hints:  Ⅎwnf 1453  {cab 2156  Ⅎwnfc 2299

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-nfc 2301

This theorem is referenced by:  nfaba1  2318  nfrabxy  2650  sbcel12g  3064  sbceqg  3065  nfun  3283  nfpw  3577  nfpr  3631  nfop  3779  nfuni  3800  nfint  3839  intab  3858  nfiunxy  3897  nfiinxy  3898  nfiunya  3899  nfiinya  3900  nfiu1  3901  nfii1  3902  nfopab  4055  nfopab1  4056  nfopab2  4057  repizf2  4146  nfdm  4853  fun11iun  5461  eusvobj2  5837  nfoprab1  5900  nfoprab2  5901  nfoprab3  5902  nfoprab  5903  nfrecs  6284  nffrec  6373  nfixpxy  6692  nfixp1  6693