Theorem nfab 2354

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

Syntax hints:  Ⅎwnf 1484  {cab 2192  Ⅎwnfc 2336

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-nfc 2338

This theorem is referenced by:  nfaba1  2355  nfrabw  2688  sbcel12g  3109  sbceqg  3110  nfun  3330  nfpw  3630  nfpr  3684  nfop  3837  nfuni  3858  nfint  3897  intab  3916  nfiunxy  3955  nfiinxy  3956  nfiunya  3957  nfiinya  3958  nfiu1  3959  nfii1  3960  nfopab  4116  nfopab1  4117  nfopab2  4118  repizf2  4210  nfdm  4927  fun11iun  5550  eusvobj2  5937  nfoprab1  6001  nfoprab2  6002  nfoprab3  6003  nfoprab  6004  nfrecs  6400  nffrec  6489  nfixpxy  6811  nfixp1  6812  nfwrd  11029