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

Theorem nfuni 4920
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 4919 . 2 (𝑥𝐴𝑥 𝐴)
41, 3ax-mp 5 1 𝑥 𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2876   cuni 4913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-uni 4914
This theorem is referenced by:  nfiota1  6508  nffrecs  8298  nfwrecsOLD  8332  nfsup  9494  ptunimpt  23590  disjabrex  32502  disjabrexf  32503  fnpreimac  32588  nfesum1  33873  nfesum2  33874  bnj1398  34879  bnj1446  34890  bnj1447  34891  bnj1448  34892  bnj1466  34898  bnj1467  34899  bnj1519  34910  bnj1520  34911  bnj1525  34914  bnj1523  34916  dfon2lem3  35609  mptsnunlem  37045  ptrest  37320  heibor1  37511  nfunidALT2  38667  nfunidALT  38668  disjinfi  44799  stoweidlem28  45649  stoweidlem59  45680  fourierdlem80  45807  saliinclf  45947  smfresal  46409  smfpimbor1lem2  46420  nfafv2  46831  nfsetrecs  48432
  Copyright terms: Public domain W3C validator