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

Theorem nfuni 4013
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 4009 . 2  |-  U. A  =  { y  |  E. z  e.  A  y  e.  z }
2 nfuni.1 . . . 4  |-  F/_ x A
3 nfv 1629 . . . 4  |-  F/ x  y  e.  z
42, 3nfrex 2753 . . 3  |-  F/ x E. z  e.  A  y  e.  z
54nfab 2575 . 2  |-  F/_ x { y  |  E. z  e.  A  y  e.  z }
61, 5nfcxfr 2568 1  |-  F/_ x U. A
Colors of variables: wff set class
Syntax hints:   {cab 2421   F/_wnfc 2558   E.wrex 2698   U.cuni 4007
This theorem is referenced by:  nfiota1  5412  nfrecs  6627  nfsup  7448  ptunimpt  17619  disjabrex  24016  disjabrexf  24017  nfesum1  24429  dfon2lem3  25404  nfwrecs  25525  heibor1  26500  stoweidlem28  27734  stoweidlem59  27765  bnj1398  29330  bnj1446  29341  bnj1447  29342  bnj1448  29343  bnj1466  29349  bnj1467  29350  bnj1519  29361  bnj1520  29362  bnj1525  29365  bnj1523  29367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-uni 4008
  Copyright terms: Public domain W3C validator