Theorem nfsn 4400

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

Syntax hints:  Ⅎwnfc 2894  {csn 4336  {cpr 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-sn 4337  df-pr 4339

This theorem is referenced by:  nfop  4577  iunopeqop  5144  nfpred  5872  nfsuc  5981  sniota  6060  dfmpt2  7473  bnj958  31479  bnj1000  31480  bnj1446  31582  bnj1447  31583  bnj1448  31584  bnj1466  31590  bnj1467  31591  nosupbnd2  32327  nfaltop  32552  stoweidlem21  40899  stoweidlem47  40925  nfdfat  41899