Theorem nfsn 4668

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 4653	. 2 ⊢ Ⅎ𝑥{𝐴, 𝐴}
4	1, 3	nfcxfr 2920	1 ⊢ Ⅎ𝑥{𝐴}

This proof depends on syntax axioms:  Ⅎwnfc 2907  {csn 4584  {cpr 4586

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  nfop  4849  iunopeqop  5498  iunopeqopOLD  5499  nfpred  6304  nfsuc  6432  sniota  6524  dfmpo  8099  nosupbnd2  27952  noinfbnd2  27967  bnj958  35449  bnj1000  35450  bnj1446  35554  bnj1447  35555  bnj1448  35556  bnj1466  35562  bnj1467  35563  nfaltop  36560  stoweidlem21  46849  stoweidlem47  46875  nfdfat  48015