Theorem nfab 2389

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

Syntax hints:  Ⅎwnf 1509  {cab 2218  Ⅎwnfc 2371

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-nfc 2373

This theorem is referenced by:  nfaba1  2390  nfrabw  2724  sbcel12g  3152  sbceqg  3153  nfun  3374  nfpw  3684  nfpr  3738  nfop  3898  nfuni  3919  nfint  3958  intab  3977  nfiunxy  4016  nfiinxy  4017  nfiunya  4018  nfiinya  4019  nfiu1  4020  nfii1  4021  nfopab  4177  nfopab1  4178  nfopab2  4179  repizf2  4274  nfdm  5000  fun11iun  5634  eusvobj2  6035  nfoprab1  6101  nfoprab2  6102  nfoprab3  6103  nfoprab  6104  nfrecs  6537  nffrec  6626  nfixpxy  6951  nfixp1  6952  nfwrd  11246