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

Theorem nfiu1 4939
 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 4907 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
2 nfre1 3298 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2988 . 2 𝑥{𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2980 1 𝑥 𝑥𝐴 𝐵
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2115  {cab 2802  Ⅎwnfc 2962  ∃wrex 3134  ∪ ciun 4905 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rex 3139  df-iun 4907 This theorem is referenced by:  ssiun2s  4958  disjxiun  5049  triun  5171  iunopeqop  5398  eliunxp  5695  opeliunxp2  5696  opeliunxp2f  7872  ixpf  8480  ixpiunwdom  9051  r1val1  9212  rankuni2b  9279  rankval4  9293  cplem2  9316  ac6num  9899  iunfo  9959  iundom2g  9960  inar1  10195  tskuni  10203  gsum2d2lem  19093  gsum2d2  19094  gsumcom2  19095  iunconn  22036  ptclsg  22223  cnextfvval  22673  ssiun2sf  30322  aciunf1lem  30418  fsumiunle  30556  esum2dlem  31408  esum2d  31409  esumiun  31410  sigapildsys  31478  bnj958  32269  bnj1000  32270  bnj981  32279  bnj1398  32363  bnj1408  32365  ralssiun  34769  iunconnlem2  41561  iunmapss  41769  iunmapsn  41771  allbutfi  41955  fsumiunss  42143  dvnprodlem1  42514  dvnprodlem2  42515  sge0iunmptlemfi  42978  sge0iunmptlemre  42980  sge0iunmpt  42983  iundjiun  43025  voliunsge0lem  43037  caratheodorylem2  43092  smflimmpt  43367  smflimsuplem7  43383  eliunxp2  44661
 Copyright terms: Public domain W3C validator