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

Theorem nfuni 4240
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 4236 . 2  |-  U. A  =  { y  |  E. z  e.  A  y  e.  z }
2 nfuni.1 . . . 4  |-  F/_ x A
3 nfv 1694 . . . 4  |-  F/ x  y  e.  z
42, 3nfrex 2906 . . 3  |-  F/ x E. z  e.  A  y  e.  z
54nfab 2609 . 2  |-  F/_ x { y  |  E. z  e.  A  y  e.  z }
61, 5nfcxfr 2603 1  |-  F/_ x U. A
Colors of variables: wff setvar class
Syntax hints:   {cab 2428   F/_wnfc 2591   E.wrex 2794   U.cuni 4234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-uni 4235
This theorem is referenced by:  nfiota1  5543  nfrecs  7046  nfsup  7913  ptunimpt  20074  disjabrex  27421  disjabrexf  27422  nfesum1  28031  dfon2lem3  29193  nfwrecs  29314  ptrest  30024  heibor1  30282  stoweidlem28  31764  stoweidlem59  31795  fourierdlem80  31923  bnj1398  33958  bnj1446  33969  bnj1447  33970  bnj1448  33971  bnj1466  33977  bnj1467  33978  bnj1519  33989  bnj1520  33990  bnj1525  33993  bnj1523  33995
  Copyright terms: Public domain W3C validator