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

Theorem nfuni 4871
Description: Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Hypothesis
Ref Expression
nfuni.1 𝑥𝐴
Assertion
Ref Expression
nfuni 𝑥 𝐴

Proof of Theorem nfuni
StepHypRef Expression
1 nfuni.1 . 2 𝑥𝐴
2 id 22 . . 3 (𝑥𝐴𝑥𝐴)
32nfunid 4870 . 2 (𝑥𝐴𝑥 𝐴)
41, 3ax-mp 5 1 𝑥 𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2886   cuni 4864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ral 3064  df-rex 3073  df-uni 4865
This theorem is referenced by:  nfiota1  6448  nffrecs  8207  nfwrecsOLD  8241  nfsup  9346  ptunimpt  22898  disjabrex  31328  disjabrexf  31329  fnpreimac  31415  nfesum1  32443  nfesum2  32444  bnj1398  33450  bnj1446  33461  bnj1447  33462  bnj1448  33463  bnj1466  33469  bnj1467  33470  bnj1519  33481  bnj1520  33482  bnj1525  33485  bnj1523  33487  dfon2lem3  34170  mptsnunlem  35741  ptrest  36009  heibor1  36201  nfunidALT2  37363  nfunidALT  37364  disjinfi  43311  stoweidlem28  44164  stoweidlem59  44195  fourierdlem80  44322  saliinclf  44462  smfresal  44924  smfpimbor1lem2  44935  nfafv2  45345  nfsetrecs  47026
  Copyright terms: Public domain W3C validator