Theorem nfab 2769

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

Syntax hints:  Ⅎwnf 1708  {cab 2608  Ⅎwnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-nfc 2753

This theorem is referenced by:  nfaba1  2770  nfun  3769  sbcel12  3983  sbceqg  3984  nfpw  4172  nfpr  4232  nfuni  4442  nfint  4486  intab  4507  nfiun  4548  nfiin  4549  nfiu1  4550  nfii1  4551  nfopab  4718  nfopab1  4719  nfopab2  4720  nfdm  5367  eusvobj2  6643  nfoprab1  6704  nfoprab2  6705  nfoprab3  6706  nfoprab  6707  fun11iun  7126  nfwrecs  7409  nfixp  7927  nfixp1  7928  reclem2pr  9870  nfwrd  13333  mreiincl  16256  lss1d  18963  disjabrex  29395  disjabrexf  29396  esumc  30113  bnj900  30999  bnj1014  31030  bnj1123  31054  bnj1307  31091  bnj1398  31102  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1447  31114  bnj1467  31122  bnj1518  31132  bnj1519  31133  dfon2lem3  31690  sdclem1  33539  heibor1  33609  dihglblem5  36587  sbcel12gOLD  38754  ssfiunibd  39523  hoidmvlelem1  40809  nfsetrecs  42433  setrec2lem2  42441  setrec2  42442