Theorem nfsn 4675

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

Syntax hints:  Ⅎwnfc 2916  {csn 4591  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-v 3465  df-un 3918  df-sn 4592  df-pr 4594

This theorem is referenced by:  nfop  4855  iunopeqop  5502  iunopeqopOLD  5503  nfpred  6304  nfsuc  6432  sniota  6524  dfmpo  8093  nosupbnd2  27842  noinfbnd2  27857  bnj958  35269  bnj1000  35270  bnj1446  35374  bnj1447  35375  bnj1448  35376  bnj1466  35382  bnj1467  35383  nfaltop  36367  stoweidlem21  46620  stoweidlem47  46646  nfdfat  47746