Theorem nfsn 4651

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

Syntax hints:  Ⅎwnfc 2883  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  nfop  4832  iunopeqop  5475  iunopeqopOLD  5476  nfpred  6270  nfsuc  6397  sniota  6489  dfmpo  8052  nosupbnd2  27680  noinfbnd2  27695  bnj958  35082  bnj1000  35083  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1466  35195  bnj1467  35196  nfaltop  36162  stoweidlem21  46449  stoweidlem47  46475  nfdfat  47575