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

Theorem nfsn 4544
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 4479 . 2 {𝐴} = {𝐴, 𝐴}
2 nfsn.1 . . 3 𝑥𝐴
32, 2nfpr 4529 . 2 𝑥{𝐴, 𝐴}
41, 3nfcxfr 2945 1 𝑥{𝐴}
Colors of variables: wff setvar class
Syntax hints:  wnfc 2931  {csn 4466  {cpr 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-un 3859  df-sn 4467  df-pr 4469
This theorem is referenced by:  nfop  4720  iunopeqop  5295  nfpred  6020  nfsuc  6129  sniota  6208  dfmpo  7644  bnj958  31784  bnj1000  31785  bnj1446  31887  bnj1447  31888  bnj1448  31889  bnj1466  31895  bnj1467  31896  nosupbnd2  32770  nfaltop  32995  stoweidlem21  41802  stoweidlem47  41828  nfdfat  42796
  Copyright terms: Public domain W3C validator