Theorem nfsn 4639

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

Syntax hints:  Ⅎwnfc 2886  {csn 4555  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-v 3433  df-un 3888  df-sn 4556  df-pr 4558

This theorem is referenced by:  nfop  4820  iunopeqop  5462  iunopeqopOLD  5463  nfpred  6257  nfsuc  6384  sniota  6476  dfmpo  8041  nosupbnd2  27698  noinfbnd2  27713  bnj958  35122  bnj1000  35123  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1466  35235  bnj1467  35236  nfaltop  36208  stoweidlem21  46464  stoweidlem47  46490  nfdfat  47590