Theorem nfsn 4544

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

Syntax hints:  Ⅎwnfc 2931  {csn 4466  {cpr 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-un 3859  df-sn 4467  df-pr 4469

This theorem is referenced by:  nfop  4720  iunopeqop  5295  nfpred  6020  nfsuc  6129  sniota  6208  dfmpo  7644  bnj958  31784  bnj1000  31785  bnj1446  31887  bnj1447  31888  bnj1448  31889  bnj1466  31895  bnj1467  31896  nosupbnd2  32770  nfaltop  32995  stoweidlem21  41802  stoweidlem47  41828  nfdfat  42796