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

Theorem iunexg 7988
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 5030 . . 3 (∀𝑥𝐴 𝐵𝑊 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
21adantl 481 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
3 abrexexg 7985 . . . 4 (𝐴𝑉 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
43uniexd 7762 . . 3 (𝐴𝑉 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
54adantr 480 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
62, 5eqeltrd 2841 1 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {cab 2714  wral 3061  wrex 3070  Vcvv 3480   cuni 4907   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-uni 4908  df-iun 4993
This theorem is referenced by:  abrexex2g  7989  opabex3d  7990  opabex3rd  7991  opabex3  7992  iunex  7993  xpexgALT  8006  mpoexxg  8100  ixpexg  8962  ixpssmapg  8968  ttrclselem2  9766  iundom  10582  iunctb  10614  wrdexg  14562  cshwsex  17138  imasplusg  17562  imasmulr  17563  imasvsca  17565  imasip  17566  gsum2d2  19992  gsumcom2  19993  dprd2da  20062  ptcls  23624  ptcmplem2  24061  elpwiuncl  32546  aciunf1lem  32672  gsumpart  33060  gsumwrd2dccat  33070  irngval  33735  esum2dlem  34093  esum2d  34094  esumiun  34095  omssubadd  34302  eulerpartlemgs2  34382  bnj535  34904  bnj546  34910  bnj893  34942  bnj1136  35011  bnj1413  35049  weiunse  36469  numiunnum  36471  eliunov2  43692  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  iunrelexp0  43715  collexd  44276  unirnmapsn  45219  iunmapss  45220  ssmapsn  45221  iunmapsn  45222  sge0iunmptlemfi  46428  sge0iunmpt  46433  smflimlem1  46786  smfliminflem  46845  mpoexxg2  48254
  Copyright terms: Public domain W3C validator