Theorem nfsn 4712

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

Syntax hints:  Ⅎwnfc 2888  {csn 4631  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  nfop  4894  iunopeqop  5531  nfpred  6328  nfsuc  6458  sniota  6554  dfmpo  8126  nosupbnd2  27776  noinfbnd2  27791  bnj958  34933  bnj1000  34934  bnj1446  35038  bnj1447  35039  bnj1448  35040  bnj1466  35046  bnj1467  35047  nfaltop  35962  stoweidlem21  45977  stoweidlem47  46003  nfdfat  47077