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

Theorem nfuni 3963
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 3959 . 2  |-  U. A  =  { y  |  E. z  e.  A  y  e.  z }
2 nfuni.1 . . . 4  |-  F/_ x A
3 nfv 1626 . . . 4  |-  F/ x  y  e.  z
42, 3nfrex 2704 . . 3  |-  F/ x E. z  e.  A  y  e.  z
54nfab 2527 . 2  |-  F/_ x { y  |  E. z  e.  A  y  e.  z }
61, 5nfcxfr 2520 1  |-  F/_ x U. A
Colors of variables: wff set class
Syntax hints:   {cab 2373   F/_wnfc 2510   E.wrex 2650   U.cuni 3957
This theorem is referenced by:  nfiota1  5360  nfrecs  6571  nfsup  7389  ptunimpt  17548  disjabrex  23868  disjabrexf  23869  nfesum1  24233  dfon2lem3  25165  heibor1  26210  stoweidlem28  27445  stoweidlem59  27476  bnj1398  28741  bnj1446  28752  bnj1447  28753  bnj1448  28754  bnj1466  28760  bnj1467  28761  bnj1519  28772  bnj1520  28773  bnj1525  28776  bnj1523  28778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-uni 3958
  Copyright terms: Public domain W3C validator