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

Theorem nfiu1 4516
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 4487 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
2 nfre1 2999 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2765 . 2 𝑥{𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2759 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  {cab 2607  wnfc 2748  wrex 2908   ciun 4485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-iun 4487
This theorem is referenced by:  ssiun2s  4530  disjxiun  4609  disjxiunOLD  4610  triun  4726  iunopeqop  4941  eliunxp  5219  opeliunxp2  5220  opeliunxp2f  7281  ixpf  7874  ixpiunwdom  8440  r1val1  8593  rankuni2b  8660  rankval4  8674  cplem2  8697  ac6num  9245  iunfo  9305  iundom2g  9306  inar1  9541  tskuni  9549  gsum2d2lem  18293  gsum2d2  18294  gsumcom2  18295  iunconn  21141  ptclsg  21328  cnextfvval  21779  ssiun2sf  29220  aciunf1lem  29301  esum2dlem  29932  esum2d  29933  esumiun  29934  sigapildsys  30003  bnj958  30715  bnj1000  30716  bnj981  30725  bnj1398  30807  bnj1408  30809  iunconnlem2  38651  iunmapss  38878  iunmapsn  38880  allbutfi  39077  fsumiunss  39208  dvnprodlem1  39464  dvnprodlem2  39465  sge0iunmptlemfi  39934  sge0iunmptlemre  39936  sge0iunmpt  39939  iundjiun  39981  voliunsge0lem  39993  caratheodorylem2  40045  smflimmpt  40320  smflimsuplem7  40336  eliunxp2  41397
  Copyright terms: Public domain W3C validator