Theorem nfsn 4661

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 4590	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		nfsn.1	. . 3 ⊢ Ⅎ𝑥𝐴
3	2, 2	nfpr 4646	. 2 ⊢ Ⅎ𝑥{𝐴, 𝐴}
4	1, 3	nfcxfr 2893	1 ⊢ Ⅎ𝑥{𝐴}

Syntax hints:  Ⅎwnfc 2880  {csn 4577  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  nfop  4842  iunopeqop  5466  nfpred  6261  nfsuc  6388  sniota  6480  dfmpo  8041  nosupbnd2  27675  noinfbnd2  27690  bnj958  35024  bnj1000  35025  bnj1446  35129  bnj1447  35130  bnj1448  35131  bnj1466  35137  bnj1467  35138  nfaltop  36096  stoweidlem21  46181  stoweidlem47  46207  nfdfat  47289