Theorem nfsn 4349

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

Syntax hints:  Ⅎwnfc 2853  {csn 4285  {cpr 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-sn 4286  df-pr 4288

This theorem is referenced by:  nfop  4525  iunopeqop  5085  nfpred  5798  nfsuc  5909  sniota  5991  dfmpt2  7387  bnj958  31238  bnj1000  31239  bnj1446  31341  bnj1447  31342  bnj1448  31343  bnj1466  31349  bnj1467  31350  nosupbnd2  32089  nfaltop  32314  stoweidlem21  40658  stoweidlem47  40684  nfdfat  41633