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

Theorem nfsn 4400
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 4349 . 2 {𝐴} = {𝐴, 𝐴}
2 nfsn.1 . . 3 𝑥𝐴
32, 2nfpr 4390 . 2 𝑥{𝐴, 𝐴}
41, 3nfcxfr 2905 1 𝑥{𝐴}
Colors of variables: wff setvar class
Syntax hints:  wnfc 2894  {csn 4336  {cpr 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-sn 4337  df-pr 4339
This theorem is referenced by:  nfop  4577  iunopeqop  5144  nfpred  5872  nfsuc  5981  sniota  6060  dfmpt2  7473  bnj958  31479  bnj1000  31480  bnj1446  31582  bnj1447  31583  bnj1448  31584  bnj1466  31590  bnj1467  31591  nosupbnd2  32327  nfaltop  32552  stoweidlem21  40899  stoweidlem47  40925  nfdfat  41899
  Copyright terms: Public domain W3C validator