Theorem nfab1 2177

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfab1	⊢ Ⅎx{x ∣ φ}

Proof of Theorem nfab1

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfsab1 2027	. 2 ⊢ Ⅎx y ∈ {x ∣ φ}
2	1	nfci 2165	1 ⊢ Ⅎx{x ∣ φ}

Syntax hints:  {cab 2023  Ⅎwnfc 2162

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-nfc 2164

This theorem is referenced by:  abid2f  2199  nfrab1  2483  elabgt  2678  elabgf  2679  nfsbc1d  2774  ss2ab  3002  abn0r  3237  euabsn  3431  iunab  3694  iinab  3709  sniota  4837  elabgft1  9232  elabgf2  9234