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

Theorem nfsn 4349
 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 4298 . 2 {𝐴} = {𝐴, 𝐴}
2 nfsn.1 . . 3 𝑥𝐴
32, 2nfpr 4339 . 2 𝑥{𝐴, 𝐴}
41, 3nfcxfr 2864 1 𝑥{𝐴}
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2853  {csn 4285  {cpr 4287 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-sn 4286  df-pr 4288 This theorem is referenced by:  nfop  4525  iunopeqop  5085  nfpred  5798  nfsuc  5909  sniota  5991  dfmpt2  7387  bnj958  31238  bnj1000  31239  bnj1446  31341  bnj1447  31342  bnj1448  31343  bnj1466  31349  bnj1467  31350  nosupbnd2  32089  nfaltop  32314  stoweidlem21  40658  stoweidlem47  40684  nfdfat  41633
 Copyright terms: Public domain W3C validator