Theorem nfsn 4712

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

Syntax hints:  Ⅎwnfc 2884  {csn 4629  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  nfop  4890  iunopeqop  5522  nfpred  6306  nfsuc  6437  sniota  6535  dfmpo  8088  nosupbnd2  27219  noinfbnd2  27234  bnj958  33951  bnj1000  33952  bnj1446  34056  bnj1447  34057  bnj1448  34058  bnj1466  34064  bnj1467  34065  nfaltop  34952  stoweidlem21  44737  stoweidlem47  44763  nfdfat  45835