Theorem nfsn 4674

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

Syntax hints:  Ⅎwnfc 2910  {csn 4590  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  nfop  4855  iunopeqop  5506  iunopeqopOLD  5507  nfpred  6309  nfsuc  6437  sniota  6529  dfmpo  8098  nosupbnd2  27861  noinfbnd2  27876  bnj958  35309  bnj1000  35310  bnj1446  35414  bnj1447  35415  bnj1448  35416  bnj1466  35422  bnj1467  35423  nfaltop  36453  stoweidlem21  46718  stoweidlem47  46744  nfdfat  47847