Theorem nfsn 4664

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

Syntax hints:  Ⅎwnfc 2883  {csn 4580  {cpr 4582

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 2184  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  nfop  4845  iunopeqop  5469  nfpred  6264  nfsuc  6391  sniota  6483  dfmpo  8044  nosupbnd2  27684  noinfbnd2  27699  bnj958  35096  bnj1000  35097  bnj1446  35201  bnj1447  35202  bnj1448  35203  bnj1466  35209  bnj1467  35210  nfaltop  36174  stoweidlem21  46265  stoweidlem47  46291  nfdfat  47373