Theorem nfsn 4623

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

Syntax hints:  Ⅎwnfc 2884  {csn 4541  {cpr 4543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-v 3410  df-un 3871  df-sn 4542  df-pr 4544

This theorem is referenced by:  nfop  4800  iunopeqop  5404  nfpred  6165  nfsuc  6284  sniota  6371  dfmpo  7870  bnj958  32633  bnj1000  32634  bnj1446  32738  bnj1447  32739  bnj1448  32740  bnj1466  32746  bnj1467  32747  nosupbnd2  33656  noinfbnd2  33671  nfaltop  34019  stoweidlem21  43237  stoweidlem47  43263  nfdfat  44291