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

Theorem iunexg 7970
Description: The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
Assertion
Ref Expression
iunexg ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem iunexg
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfiun2g 5010 . . 3 (∀𝑥𝐴 𝐵𝑊 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
21adantl 481 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
3 abrexexg 7967 . . . 4 (𝐴𝑉 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
43uniexd 7744 . . 3 (𝐴𝑉 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
54adantr 480 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
62, 5eqeltrd 2833 1 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539  wcel 2107  {cab 2712  wral 3050  wrex 3059  Vcvv 3463   cuni 4887   ciun 4971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-11 2156  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-un 7737
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-mo 2538  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-v 3465  df-ss 3948  df-uni 4888  df-iun 4973
This theorem is referenced by:  abrexex2g  7971  opabex3d  7972  opabex3rd  7973  opabex3  7974  iunex  7975  xpexgALT  7988  mpoexxg  8082  ixpexg  8944  ixpssmapg  8950  ttrclselem2  9748  iundom  10564  iunctb  10596  wrdexg  14545  cshwsex  17121  imasplusg  17534  imasmulr  17535  imasvsca  17537  imasip  17538  gsum2d2  19961  gsumcom2  19962  dprd2da  20031  ptcls  23571  ptcmplem2  24008  elpwiuncl  32475  aciunf1lem  32608  gsumpart  33004  gsumwrd2dccat  33014  irngval  33677  esum2dlem  34068  esum2d  34069  esumiun  34070  omssubadd  34277  eulerpartlemgs2  34357  bnj535  34879  bnj546  34885  bnj893  34917  bnj1136  34986  bnj1413  35024  weiunse  36444  numiunnum  36446  eliunov2  43669  fvmptiunrelexplb0d  43674  fvmptiunrelexplb1d  43676  iunrelexp0  43692  collexd  44248  unirnmapsn  45191  iunmapss  45192  ssmapsn  45193  iunmapsn  45194  sge0iunmptlemfi  46400  sge0iunmpt  46405  smflimlem1  46758  smfliminflem  46817  mpoexxg2  48227
  Copyright terms: Public domain W3C validator