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

Syntax hints:  Ⅎwnfc 2876  {csn 4579  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  nfop  4843  iunopeqop  5468  nfpred  6258  nfsuc  6385  sniota  6477  dfmpo  8042  nosupbnd2  27644  noinfbnd2  27659  bnj958  34909  bnj1000  34910  bnj1446  35014  bnj1447  35015  bnj1448  35016  bnj1466  35022  bnj1467  35023  nfaltop  35956  stoweidlem21  46006  stoweidlem47  46032  nfdfat  47115