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

Theorem nfsn 4379
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 4329 . 2 {𝐴} = {𝐴, 𝐴}
2 nfsn.1 . . 3 𝑥𝐴
32, 2nfpr 4369 . 2 𝑥{𝐴, 𝐴}
41, 3nfcxfr 2911 1 𝑥{𝐴}
Colors of variables: wff setvar class
Syntax hints:  wnfc 2900  {csn 4316  {cpr 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-pr 4319
This theorem is referenced by:  nfop  4555  iunopeqop  5114  nfpred  5826  nfsuc  5937  sniota  6019  dfmpt2  7416  bnj958  31341  bnj1000  31342  bnj1446  31444  bnj1447  31445  bnj1448  31446  bnj1466  31452  bnj1467  31453  nosupbnd2  32192  nfaltop  32417  stoweidlem21  40748  stoweidlem47  40774  nfdfat  41723
  Copyright terms: Public domain W3C validator