Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfsn Structured version   Visualization version   GIF version

Theorem nfsn 4606
 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
StepHypRef Expression
1 dfsn2 4541 . 2 {𝐴} = {𝐴, 𝐴}
2 nfsn.1 . . 3 𝑥𝐴
32, 2nfpr 4591 . 2 𝑥{𝐴, 𝐴}
41, 3nfcxfr 2953 1 𝑥{𝐴}
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2936  {csn 4528  {cpr 4530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3444  df-un 3888  df-sn 4529  df-pr 4531 This theorem is referenced by:  nfop  4785  iunopeqop  5380  nfpred  6128  nfsuc  6237  sniota  6323  dfmpo  7793  bnj958  32388  bnj1000  32389  bnj1446  32493  bnj1447  32494  bnj1448  32495  bnj1466  32501  bnj1467  32502  nosupbnd2  33406  noinfbnd2  33421  nfaltop  33701  stoweidlem21  42831  stoweidlem47  42857  nfdfat  43851
 Copyright terms: Public domain W3C validator