Theorem nfsn 4379

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

Syntax hints:  Ⅎwnfc 2900  {csn 4316  {cpr 4318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-pr 4319

This theorem is referenced by:  nfop  4555  iunopeqop  5114  nfpred  5826  nfsuc  5937  sniota  6019  dfmpt2  7416  bnj958  31341  bnj1000  31342  bnj1446  31444  bnj1447  31445  bnj1448  31446  bnj1466  31452  bnj1467  31453  nosupbnd2  32192  nfaltop  32417  stoweidlem21  40748  stoweidlem47  40774  nfdfat  41723