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

Theorem iunexg 7806
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 4960 . . 3 (∀𝑥𝐴 𝐵𝑊 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
21adantl 482 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
3 abrexexg 7803 . . . 4 (𝐴𝑉 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
43uniexd 7595 . . 3 (𝐴𝑉 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
54adantr 481 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
62, 5eqeltrd 2839 1 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  wcel 2106  {cab 2715  wral 3064  wrex 3065  Vcvv 3432   cuni 4839   ciun 4924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-iun 4926
This theorem is referenced by:  abrexex2g  7807  opabex3d  7808  opabex3rd  7809  opabex3  7810  iunex  7811  xpexgALT  7824  mpoexxg  7916  ixpexg  8710  ixpssmapg  8716  ttrclselem2  9484  iundom  10298  iunctb  10330  wrdexg  14227  cshwsex  16802  imasplusg  17228  imasmulr  17229  imasvsca  17231  imasip  17232  gsum2d2  19575  gsumcom2  19576  dprd2da  19645  ptcls  22767  ptcmplem2  23204  elpwiuncl  30876  aciunf1lem  30999  gsumpart  31315  esum2dlem  32060  esum2d  32061  esumiun  32062  omssubadd  32267  eulerpartlemgs2  32347  bnj535  32870  bnj546  32876  bnj893  32908  bnj1136  32977  bnj1413  33015  eliunov2  41287  fvmptiunrelexplb0d  41292  fvmptiunrelexplb1d  41294  iunrelexp0  41310  collexd  41875  unirnmapsn  42754  iunmapss  42755  ssmapsn  42756  iunmapsn  42757  sge0iunmptlemfi  43951  sge0iunmpt  43956  smflimlem1  44306  smfliminflem  44363  mpoexxg2  45673
  Copyright terms: Public domain W3C validator