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

Theorem nfiu1 4299
 Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
Assertion
Ref Expression
nfiu1

Proof of Theorem nfiu1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-iun 4271 . 2
2 nfre1 2846 . . 3
32nfab 2616 . 2
41, 3nfcxfr 2610 1
 Colors of variables: wff setvar class Syntax hints:   wcel 1904  cab 2457  wnfc 2599  wrex 2757  ciun 4269 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-iun 4271 This theorem is referenced by:  ssiun2s  4313  disjxiun  4392  triun  4503  eliunxp  4977  opeliunxp2  4978  opeliunxp2f  6975  ixpf  7562  ixpiunwdom  8124  r1val1  8275  rankuni2b  8342  rankval4  8356  cplem2  8379  ac6num  8927  iunfo  8982  iundom2g  8983  inar1  9218  tskuni  9226  gsum2d2lem  17683  gsum2d2  17684  gsumcom2  17685  iuncon  20520  ptclsg  20707  cnextfvval  21158  ssiun2sf  28252  aciunf1lem  28339  esum2dlem  28987  esum2d  28988  esumiun  28989  sigapildsys  29058  bnj958  29823  bnj1000  29824  bnj981  29833  bnj1398  29915  bnj1408  29917  iunconlem2  37395  iunmapss  37568  iunmapsn  37570  fsumiunss  37750  dvnprodlem1  37918  dvnprodlem2  37919  sge0iunmptlemfi  38369  sge0iunmptlemre  38371  sge0iunmpt  38374  iundjiun  38414  voliunsge0lem  38426  caratheodorylem2  38467  iunopeqop  39151  eliunxp2  40623
 Copyright terms: Public domain W3C validator