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

Theorem iuneq2dv 4513
 Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
Hypothesis
Ref Expression
iuneq2dv.1 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
iuneq2dv (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2dv
StepHypRef Expression
1 iuneq2dv.1 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
21ralrimiva 2965 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
3 iuneq2 4508 . 2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
42, 3syl 17 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1992  ∀wral 2912  ∪ ciun 4490 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-v 3193  df-in 3567  df-ss 3574  df-iun 4492 This theorem is referenced by:  iuneq12d  4517  iuneq2d  4518  fparlem3  7225  fparlem4  7226  oalim  7558  omlim  7559  oelim  7560  oelim2  7621  r1val3  8646  imasdsval  16091  acsfn  16236  tgidm  20690  cmpsub  21108  alexsublem  21753  bcth3  23031  ovoliunlem1  23172  voliunlem1  23220  uniiccdif  23247  uniioombllem2  23252  uniioombllem3a  23253  uniioombllem4  23255  itg2monolem1  23418  taylpfval  24018  ofpreima2  29300  esum2dlem  29927  eulerpartlemgu  30212  cvmscld  30955  msubvrs  31157  mblfinlem2  33065  ftc1anclem6  33108  heibor  33238  trclfvcom  37482  meaiininclem  39994  carageniuncllem2  40030  hoidmv1le  40102  hoidmvle  40108  ovnhoilem2  40110  ovnhoi  40111  ovnlecvr2  40118  ovncvr2  40119  hspmbl  40137  ovolval4lem1  40157  ovnovollem1  40164  ovnovollem2  40165  iunhoiioo  40184  vonioolem2  40189  smflimlem4  40276  smflimlem6  40278
 Copyright terms: Public domain W3C validator