Theorem nfsn 4671

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

Syntax hints:  Ⅎwnfc 2876  {csn 4589  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  nfop  4853  iunopeqop  5481  nfpred  6279  nfsuc  6406  sniota  6502  dfmpo  8081  nosupbnd2  27628  noinfbnd2  27643  bnj958  34930  bnj1000  34931  bnj1446  35035  bnj1447  35036  bnj1448  35037  bnj1466  35043  bnj1467  35044  nfaltop  35968  stoweidlem21  46019  stoweidlem47  46045  nfdfat  47128