Theorem nfsn 4663

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 4648	. 2 ⊢ Ⅎ𝑥{𝐴, 𝐴}
4	1, 3	nfcxfr 2921	1 ⊢ Ⅎ𝑥{𝐴}

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3455  df-un 3907  df-sn 4580  df-pr 4582

This theorem is referenced by:  nfop  4844  iunopeqop  5487  iunopeqopOLD  5488  nfpred  6288  nfsuc  6415  sniota  6507  dfmpo  8075  nosupbnd2  27768  noinfbnd2  27783  bnj958  35196  bnj1000  35197  bnj1446  35301  bnj1447  35302  bnj1448  35303  bnj1466  35309  bnj1467  35310  nfaltop  36291  stoweidlem21  46556  stoweidlem47  46582  nfdfat  47682