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

Theorem nfiu1 4121
Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
Assertion
Ref Expression
nfiu1  |-  F/_ x U_ x  e.  A  B

Proof of Theorem nfiu1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-iun 4095 . 2  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
2 nfre1 2762 . . 3  |-  F/ x E. x  e.  A  y  e.  B
32nfab 2576 . 2  |-  F/_ x { y  |  E. x  e.  A  y  e.  B }
41, 3nfcxfr 2569 1  |-  F/_ x U_ x  e.  A  B
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   {cab 2422   F/_wnfc 2559   E.wrex 2706   U_ciun 4093
This theorem is referenced by:  ssiun2s  4135  disjxiun  4209  triun  4315  eliunxp  5012  opeliunxp2  5013  ixpf  7084  ixpiunwdom  7559  r1val1  7712  rankuni2b  7779  rankval4  7793  cplem2  7814  ac6num  8359  iunfo  8414  iundom2g  8415  inar1  8650  tskuni  8658  gsum2d2lem  15547  gsum2d2  15548  gsumcom2  15549  iuncon  17491  ptclsg  17647  cnextfvval  18096  ssiun2sf  24010  iunconlem2  29047  bnj958  29311  bnj1000  29312  bnj981  29321  bnj1398  29403  bnj1408  29405
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-iun 4095
  Copyright terms: Public domain W3C validator