Theorem nfsn 4648

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

Syntax hints:  Ⅎwnfc 2888  {csn 4566  {cpr 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-v 3432  df-un 3896  df-sn 4567  df-pr 4569

This theorem is referenced by:  nfop  4825  iunopeqop  5437  nfpred  6204  nfsuc  6334  sniota  6421  dfmpo  7926  bnj958  32899  bnj1000  32900  bnj1446  33004  bnj1447  33005  bnj1448  33006  bnj1466  33012  bnj1467  33013  nosupbnd2  33898  noinfbnd2  33913  nfaltop  34261  stoweidlem21  43516  stoweidlem47  43542  nfdfat  44570