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

Theorem nfsn 4040
Description: Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
Hypothesis
Ref Expression
nfsn.1  |-  F/_ x A
Assertion
Ref Expression
nfsn  |-  F/_ x { A }

Proof of Theorem nfsn
StepHypRef Expression
1 dfsn2 3992 . 2  |-  { A }  =  { A ,  A }
2 nfsn.1 . . 3  |-  F/_ x A
32, 2nfpr 4030 . 2  |-  F/_ x { A ,  A }
41, 3nfcxfr 2600 1  |-  F/_ x { A }
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2589   {csn 3979   {cpr 3981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-sn 3980  df-pr 3982
This theorem is referenced by:  nfop  4195  nfpred  5403  nfsuc  5512  sniota  5591  dfmpt2  6912  bnj958  29799  bnj1000  29800  bnj1446  29902  bnj1447  29903  bnj1448  29904  bnj1466  29910  bnj1467  29911  nfaltop  30795  stoweidlem21  37918  stoweidlem47  37945  nfdfat  38669  iunopeqop  39044
  Copyright terms: Public domain W3C validator