Theorem nfab 2932

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

Syntax hints:  Ⅎwnf 1746  {cab 2752  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-nfc 2912

This theorem is referenced by:  nfaba1  2933  nfun  4024  sbcel12  4240  sbceqg  4241  nfpw  4430  nfpr  4498  nfuni  4714  nfint  4755  intab  4775  nfiun  4817  nfiin  4818  nfiu1  4819  nfii1  4820  nfopab  4993  nfopab1  4994  nfopab2  4995  nfdm  5663  eusvobj2  6967  nfoprab1  7032  nfoprab2  7033  nfoprab3  7034  nfoprab  7035  fun11iun  7456  nfwrecs  7750  nfixp  8276  nfixp1  8277  reclem2pr  10266  nfwrd  13703  mreiincl  16737  lss1d  19469  disjabrex  30112  disjabrexf  30113  esumc  30983  bnj900  31877  bnj1014  31908  bnj1123  31932  bnj1307  31969  bnj1398  31980  bnj1444  31989  bnj1445  31990  bnj1446  31991  bnj1447  31992  bnj1467  32000  bnj1518  32010  bnj1519  32011  dfon2lem3  32579  nffrecs  32670  sdclem1  34489  heibor1  34559  dihglblem5  37908  ssfiunibd  41030  hoidmvlelem1  42333  nfsetrecs  44181  setrec2lem2  44189  setrec2  44190