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

Theorem iunex 7893
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 7888 . 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 2708  ax-rep 5240  ax-sep 5254  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-mo 2539  df-clab 2715  df-cleq 2729  df-clel 2815  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  9623  tz9.1c  9624  cplem2  9784  fseqdom  9920  pwsdompw  10098  cfsmolem  10164  ac6c4  10375  konigthlem  10462  alephreg  10476  pwfseqlem4  10556  pwfseqlem5  10557  pwxpndom2  10559  wunex2  10632  wuncval2  10641  inar1  10669  rtrclreclem1  14902  dfrtrclrec2  14903  rtrclreclem2  14904  rtrclreclem4  14906  isfunc  17710  smndex1bas  18676  smndex1sgrp  18678  smndex1mnd  18680  smndex1id  18681  dfac14  22921  txcmplem2  22945  cnextfval  23365  bnj893  33352  colinearex  34583  volsupnfl  36061  heiborlem3  36210  comptiunov2i  41889  corclrcl  41890  iunrelexpmin1  41891  trclrelexplem  41894  iunrelexpmin2  41895  dftrcl3  41903  trclfvcom  41906  cnvtrclfv  41907  cotrcltrcl  41908  trclimalb2  41909  trclfvdecomr  41911  dfrtrcl3  41916  dfrtrcl4  41921  corcltrcl  41922  cotrclrcl  41925  carageniuncllem1  44663  carageniuncllem2  44664  carageniuncl  44665  caratheodorylem1  44668  caratheodorylem2  44669  ovnovollem1  44798  ovnovollem2  44799  smfresal  44930
  Copyright terms: Public domain W3C validator