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  3579  nfpr  3633  nfop  3781  nfuni  3802  nfint  3841  intab  3860  nfiunxy  3899  nfiinxy  3900  nfiunya  3901  nfiinya  3902  nfiu1  3903  nfii1  3904  nfopab  4057  nfopab1  4058  nfopab2  4059  repizf2  4148  nfdm  4855  fun11iun  5463  eusvobj2  5839  nfoprab1  5902  nfoprab2  5903  nfoprab3  5904  nfoprab  5905  nfrecs  6286  nffrec  6375  nfixpxy  6695  nfixp1  6696