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

Theorem nfuni 4251
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 4247 . 2  |-  U. A  =  { y  |  E. z  e.  A  y  e.  z }
2 nfuni.1 . . . 4  |-  F/_ x A
3 nfv 1683 . . . 4  |-  F/ x  y  e.  z
42, 3nfrex 2927 . . 3  |-  F/ x E. z  e.  A  y  e.  z
54nfab 2633 . 2  |-  F/_ x { y  |  E. z  e.  A  y  e.  z }
61, 5nfcxfr 2627 1  |-  F/_ x U. A
Colors of variables: wff setvar class
Syntax hints:   {cab 2452   F/_wnfc 2615   E.wrex 2815   U.cuni 4245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-uni 4246
This theorem is referenced by:  nfiota1  5553  nfrecs  7044  nfsup  7911  ptunimpt  19859  disjabrex  27144  disjabrexf  27145  nfesum1  27721  dfon2lem3  28822  nfwrecs  28943  ptrest  29653  heibor1  29937  stoweidlem28  31356  stoweidlem59  31387  fourierdlem80  31515  bnj1398  33187  bnj1446  33198  bnj1447  33199  bnj1448  33200  bnj1466  33206  bnj1467  33207  bnj1519  33218  bnj1520  33219  bnj1525  33222  bnj1523  33224
  Copyright terms: Public domain W3C validator