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

Theorem nfsn 4213
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 4161 . 2 {𝐴} = {𝐴, 𝐴}
2 nfsn.1 . . 3 𝑥𝐴
32, 2nfpr 4203 . 2 𝑥{𝐴, 𝐴}
41, 3nfcxfr 2759 1 𝑥{𝐴}
Colors of variables: wff setvar class
Syntax hints:  wnfc 2748  {csn 4148  {cpr 4150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-sn 4149  df-pr 4151
This theorem is referenced by:  nfop  4386  iunopeqop  4941  nfpred  5644  nfsuc  5755  sniota  5837  dfmpt2  7212  bnj958  30718  bnj1000  30719  bnj1446  30821  bnj1447  30822  bnj1448  30823  bnj1466  30829  bnj1467  30830  nfaltop  31729  stoweidlem21  39545  stoweidlem47  39571  nfdfat  40514
  Copyright terms: Public domain W3C validator