Theorem nfsn 4647

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

Syntax hints:  Ⅎwnfc 2885  {csn 4565  {cpr 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-v 3439  df-un 3897  df-sn 4566  df-pr 4568

This theorem is referenced by:  nfop  4825  iunopeqop  5448  nfpred  6222  nfsuc  6352  sniota  6449  dfmpo  7974  bnj958  32969  bnj1000  32970  bnj1446  33074  bnj1447  33075  bnj1448  33076  bnj1466  33082  bnj1467  33083  nosupbnd2  33968  noinfbnd2  33983  nfaltop  34331  stoweidlem21  43791  stoweidlem47  43817  nfdfat  44863