Theorem nfsn 4660

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

Syntax hints:  Ⅎwnfc 2879  {csn 4576  {cpr 4578

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  nfop  4841  iunopeqop  5461  nfpred  6253  nfsuc  6380  sniota  6472  dfmpo  8032  nosupbnd2  27656  noinfbnd2  27671  bnj958  34950  bnj1000  34951  bnj1446  35055  bnj1447  35056  bnj1448  35057  bnj1466  35063  bnj1467  35064  nfaltop  36020  stoweidlem21  46065  stoweidlem47  46091  nfdfat  47164