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

Theorem nfuni 4831
 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 4830 . 2 (𝑥𝐴𝑥 𝐴)
41, 3ax-mp 5 1 𝑥 𝐴
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2962  ∪ cuni 4824 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-uni 4825 This theorem is referenced by:  nfiota1  6306  nfwrecs  7947  nfsup  8914  ptunimpt  22209  disjabrex  30351  disjabrexf  30352  fnpreimac  30435  nfesum1  31384  nfesum2  31385  bnj1398  32391  bnj1446  32402  bnj1447  32403  bnj1448  32404  bnj1466  32410  bnj1467  32411  bnj1519  32422  bnj1520  32423  bnj1525  32426  bnj1523  32428  dfon2lem3  33115  nffrecs  33205  mptsnunlem  34727  ptrest  35028  heibor1  35220  nfunidALT2  36237  nfunidALT  36238  disjinfi  41772  stoweidlem28  42623  stoweidlem59  42654  fourierdlem80  42781  smfresal  43373  smfpimbor1lem2  43384  nfafv2  43727  nfsetrecs  45169
 Copyright terms: Public domain W3C validator