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

Theorem iunex 7897
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 3066 . 2 𝑥𝐴 𝐵 ∈ V
4 iunexg 7892 . 2 ((𝐴 ∈ V ∧ ∀𝑥𝐴 𝐵 ∈ V) → 𝑥𝐴 𝐵 ∈ V)
51, 3, 4mp2an 690 1 𝑥𝐴 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  wral 3062  Vcvv 3443   ciun 4952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-un 7668
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-mo 2538  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-v 3445  df-in 3915  df-ss 3925  df-uni 4864  df-iun 4954
This theorem is referenced by:  tz9.1  9661  tz9.1c  9662  cplem2  9822  fseqdom  9958  pwsdompw  10136  cfsmolem  10202  ac6c4  10413  konigthlem  10500  alephreg  10514  pwfseqlem4  10594  pwfseqlem5  10595  pwxpndom2  10597  wunex2  10670  wuncval2  10679  inar1  10707  rtrclreclem1  14934  dfrtrclrec2  14935  rtrclreclem2  14936  rtrclreclem4  14938  isfunc  17742  smndex1bas  18708  smndex1sgrp  18710  smndex1mnd  18712  smndex1id  18713  dfac14  22953  txcmplem2  22977  cnextfval  23397  bnj893  33409  colinearex  34612  volsupnfl  36090  heiborlem3  36239  comptiunov2i  41920  corclrcl  41921  iunrelexpmin1  41922  trclrelexplem  41925  iunrelexpmin2  41926  dftrcl3  41934  trclfvcom  41937  cnvtrclfv  41938  cotrcltrcl  41939  trclimalb2  41940  trclfvdecomr  41942  dfrtrcl3  41947  dfrtrcl4  41952  corcltrcl  41953  cotrclrcl  41956  carageniuncllem1  44694  carageniuncllem2  44695  carageniuncl  44696  caratheodorylem1  44699  caratheodorylem2  44700  ovnovollem1  44829  ovnovollem2  44830  smfresal  44961
  Copyright terms: Public domain W3C validator