Theorem nfsn 4664

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 4593	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		nfsn.1	. . 3 ⊢ Ⅎ𝑥𝐴
3	2, 2	nfpr 4649	. 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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  nfop  4848  iunopeqop  5493  iunopeqopOLD  5494  nfpred  6309  nfsuc  6437  sniota  6530  dfmpo  8116  nosupbnd2  28079  noinfbnd2  28094  bnj958  35617  bnj1000  35618  bnj1446  35722  bnj1447  35723  bnj1448  35724  bnj1466  35730  bnj1467  35731  nfaltop  36838  stoweidlem21  47125  stoweidlem47  47151  nfdfat  48291