Theorem nfsn 4668

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

This proof depends on syntax axioms:  Ⅎwnfc 2908  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  nfop  4849  iunopeqop  5494  iunopeqopOLD  5495  nfpred  6308  nfsuc  6436  sniota  6528  dfmpo  8111  nosupbnd2  28066  noinfbnd2  28081  bnj958  35563  bnj1000  35564  bnj1446  35668  bnj1447  35669  bnj1448  35670  bnj1466  35676  bnj1467  35677  nfaltop  36725  stoweidlem21  47000  stoweidlem47  47026  nfdfat  48166