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 2925	1 ⊢ Ⅎ𝑥{𝐴}

This proof depends on syntax axioms:  Ⅎwnfc 2912  {csn 4591  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  nfop  4856  iunopeqop  5506  iunopeqopOLD  5507  nfpred  6311  nfsuc  6439  sniota  6531  dfmpo  8099  nosupbnd2  27911  noinfbnd2  27926  bnj958  35369  bnj1000  35370  bnj1446  35474  bnj1447  35475  bnj1448  35476  bnj1466  35482  bnj1467  35483  nfaltop  36485  stoweidlem21  46768  stoweidlem47  46794  nfdfat  47897