Theorem nfab 2755

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

Syntax hints:  Ⅎwnf 1699  {cab 2596  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-nfc 2740

This theorem is referenced by:  nfaba1  2756  nfun  3731  sbcel12  3935  sbceqg  3936  nfpw  4120  nfpr  4179  nfuni  4378  nfint  4421  intab  4442  nfiun  4484  nfiin  4485  nfiu1  4486  nfii1  4487  nfopab  4650  nfopab1  4651  nfopab2  4652  nfdm  5288  eusvobj2  6542  nfoprab1  6602  nfoprab2  6603  nfoprab3  6604  nfoprab  6605  fun11iun  7019  nfwrecs  7296  nfixp  7813  nfixp1  7814  reclem2pr  9749  nfwrd  13188  mreiincl  16079  lss1d  18784  disjabrex  28777  disjabrexf  28778  esumc  29440  bnj900  30253  bnj1014  30284  bnj1123  30308  bnj1307  30345  bnj1398  30356  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1447  30368  bnj1467  30376  bnj1518  30386  bnj1519  30387  dfon2lem3  30934  bj-xnex  32245  sdclem1  32709  heibor1  32779  dihglblem5  35605  sbcel12gOLD  37775  ssfiunibd  38464  hoidmvlelem1  39485  nfsetrecs  42232  setrec2lem2  42240  setrec2  42241