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

Theorem iunex 7017
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 2908 . 2 𝑥𝐴 𝐵 ∈ V
4 iunexg 7013 . 2 ((𝐴 ∈ V ∧ ∀𝑥𝐴 𝐵 ∈ V) → 𝑥𝐴 𝐵 ∈ V)
51, 3, 4mp2an 704 1 𝑥𝐴 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  wral 2896  Vcvv 3173   ciun 4450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798
This theorem is referenced by:  abrexex2  7018  tz9.1  8466  tz9.1c  8467  cplem2  8614  fseqdom  8710  pwsdompw  8887  cfsmolem  8953  ac6c4  9164  konigthlem  9247  alephreg  9261  pwfseqlem4  9341  pwfseqlem5  9342  pwxpndom2  9344  wunex2  9417  wuncval2  9426  inar1  9454  dfrtrclrec2  13594  rtrclreclem1  13595  rtrclreclem2  13596  rtrclreclem4  13598  isfunc  16296  dfac14  21179  txcmplem2  21203  cnextfval  21624  bnj893  30046  colinearex  31131  volsupnfl  32418  heiborlem3  32576  comptiunov2i  36811  corclrcl  36812  iunrelexpmin1  36813  trclrelexplem  36816  iunrelexpmin2  36817  dftrcl3  36825  trclfvcom  36828  cnvtrclfv  36829  cotrcltrcl  36830  trclimalb2  36831  trclfvdecomr  36833  dfrtrcl3  36838  dfrtrcl4  36843  corcltrcl  36844  cotrclrcl  36847  carageniuncllem1  39205  carageniuncllem2  39206  carageniuncl  39207  caratheodorylem1  39210  caratheodorylem2  39211  ovnovollem1  39340  ovnovollem2  39341  smfresal  39467
  Copyright terms: Public domain W3C validator