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

Theorem iunex 7993
Description: The existence of an indexed union. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be read informally as 𝐵(𝑥). (Contributed by NM, 13-Oct-2003.)
Hypotheses
Ref Expression
iunex.1 𝐴 ∈ V
iunex.2 𝐵 ∈ V
Assertion
Ref Expression
iunex 𝑥𝐴 𝐵 ∈ V
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iunex
StepHypRef Expression
1 iunex.1 . 2 𝐴 ∈ V
2 iunex.2 . . 3 𝐵 ∈ V
32rgenw 3065 . 2 𝑥𝐴 𝐵 ∈ V
4 iunexg 7988 . 2 ((𝐴 ∈ V ∧ ∀𝑥𝐴 𝐵 ∈ V) → 𝑥𝐴 𝐵 ∈ V)
51, 3, 4mp2an 692 1 𝑥𝐴 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  wral 3061  Vcvv 3480   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:  tz9.1  9769  tz9.1c  9770  cplem2  9930  fseqdom  10066  pwsdompw  10243  cfsmolem  10310  ac6c4  10521  konigthlem  10608  alephreg  10622  pwfseqlem4  10702  pwfseqlem5  10703  pwxpndom2  10705  wunex2  10778  wuncval2  10787  inar1  10815  rtrclreclem1  15096  dfrtrclrec2  15097  rtrclreclem2  15098  rtrclreclem4  15100  isfunc  17909  smndex1bas  18919  smndex1sgrp  18921  smndex1mnd  18923  smndex1id  18924  dfac14  23626  txcmplem2  23650  cnextfval  24070  bnj893  34942  colinearex  36061  volsupnfl  37672  heiborlem3  37820  comptiunov2i  43719  corclrcl  43720  iunrelexpmin1  43721  trclrelexplem  43724  iunrelexpmin2  43725  dftrcl3  43733  trclfvcom  43736  cnvtrclfv  43737  cotrcltrcl  43738  trclimalb2  43739  trclfvdecomr  43741  dfrtrcl3  43746  dfrtrcl4  43751  corcltrcl  43752  cotrclrcl  43755  carageniuncllem1  46536  carageniuncllem2  46537  carageniuncl  46538  caratheodorylem1  46541  caratheodorylem2  46542  ovnovollem1  46671  ovnovollem2  46672  smfresal  46803
  Copyright terms: Public domain W3C validator