Theorem nfab 2918

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

Syntax hints:  Ⅎwnf 1856  {cab 2757  Ⅎwnfc 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-nfc 2902

This theorem is referenced by:  nfaba1  2919  nfun  3920  sbcel12  4127  sbceqg  4128  nfpw  4311  nfpr  4369  nfuni  4580  nfint  4621  intab  4641  nfiun  4682  nfiin  4683  nfiu1  4684  nfii1  4685  nfopab  4852  nfopab1  4853  nfopab2  4854  nfdm  5503  eusvobj2  6784  nfoprab1  6849  nfoprab2  6850  nfoprab3  6851  nfoprab  6852  fun11iun  7271  nfwrecs  7559  nfixp  8079  nfixp1  8080  reclem2pr  10070  nfwrd  13522  mreiincl  16457  lss1d  19169  disjabrex  29726  disjabrexf  29727  esumc  30446  bnj900  31330  bnj1014  31361  bnj1123  31385  bnj1307  31422  bnj1398  31433  bnj1444  31442  bnj1445  31443  bnj1446  31444  bnj1447  31445  bnj1467  31453  bnj1518  31463  bnj1519  31464  dfon2lem3  32019  nffrecs  32108  sdclem1  33864  heibor1  33934  dihglblem5  37101  sbcel12gOLD  39272  ssfiunibd  40033  hoidmvlelem1  41322  nfsetrecs  42954  setrec2lem2  42962  setrec2  42963