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

Theorem nfuni 4169
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  |-  F/_ x A
Assertion
Ref Expression
nfuni  |-  F/_ x U. A

Proof of Theorem nfuni
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfuni2 4165 . 2  |-  U. A  =  { y  |  E. z  e.  A  y  e.  z }
2 nfuni.1 . . . 4  |-  F/_ x A
3 nfv 1715 . . . 4  |-  F/ x  y  e.  z
42, 3nfrex 2845 . . 3  |-  F/ x E. z  e.  A  y  e.  z
54nfab 2548 . 2  |-  F/_ x { y  |  E. z  e.  A  y  e.  z }
61, 5nfcxfr 2542 1  |-  F/_ x U. A
Colors of variables: wff setvar class
Syntax hints:   {cab 2367   F/_wnfc 2530   E.wrex 2733   U.cuni 4163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738  df-uni 4164
This theorem is referenced by:  nfiota1  5462  nfrecs  6962  nfsup  7825  ptunimpt  20181  disjabrex  27572  disjabrexf  27573  nfesum1  28188  nfesum2  28189  dfon2lem3  29382  nfwrecs  29503  ptrest  30213  heibor1  30472  stoweidlem28  31976  stoweidlem59  32007  fourierdlem80  32135  bnj1398  34437  bnj1446  34448  bnj1447  34449  bnj1448  34450  bnj1466  34456  bnj1467  34457  bnj1519  34468  bnj1520  34469  bnj1525  34472  bnj1523  34474
  Copyright terms: Public domain W3C validator