Theorem nfsn 4669

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

This proof depends on syntax axioms:  Ⅎwnfc 2911  {csn 4588  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  nfop  4854  iunopeqop  5501  iunopeqopOLD  5502  nfpred  6335  nfsuc  6463  sniota  6557  dfmpo  8150  nosupbnd2  28130  noinfbnd2  28145  bnj958  35681  bnj1000  35682  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1466  35794  bnj1467  35795  nfaltop  36960  stoweidlem21  47304  stoweidlem47  47330  nfdfat  48470