Theorem nfsn 4673

Description: Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)

Hypothesis

Ref	Expression
nfsn.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfsn	⊢ Ⅎ𝑥{𝐴}

Proof of Theorem nfsn

Step	Hyp	Ref	Expression
1		dfsn2 4604	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		nfsn.1	. . 3 ⊢ Ⅎ𝑥𝐴
3	2, 2	nfpr 4656	. 2 ⊢ Ⅎ𝑥{𝐴, 𝐴}
4	1, 3	nfcxfr 2900	1 ⊢ Ⅎ𝑥{𝐴}

Syntax hints:  Ⅎwnfc 2882  {csn 4591  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-v 3448  df-un 3918  df-sn 4592  df-pr 4594

This theorem is referenced by:  nfop  4851  iunopeqop  5483  nfpred  6263  nfsuc  6394  sniota  6492  dfmpo  8039  nosupbnd2  27101  noinfbnd2  27116  bnj958  33641  bnj1000  33642  bnj1446  33746  bnj1447  33747  bnj1448  33748  bnj1466  33754  bnj1467  33755  nfaltop  34641  stoweidlem21  44382  stoweidlem47  44408  nfdfat  45479