Theorem nfsn 4732

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

Syntax hints:  Ⅎwnfc 2893  {csn 4648  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  nfop  4913  iunopeqop  5540  nfpred  6337  nfsuc  6467  sniota  6564  dfmpo  8143  nosupbnd2  27779  noinfbnd2  27794  bnj958  34916  bnj1000  34917  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1466  35029  bnj1467  35030  nfaltop  35944  stoweidlem21  45942  stoweidlem47  45968  nfdfat  47042