MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iuneq2d Structured version   Unicode version

Theorem iuneq2d 4298
Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
Hypothesis
Ref Expression
iuneq2d.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
iuneq2d  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Distinct variable groups:    ph, x    x, A
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem iuneq2d
StepHypRef Expression
1 iuneq2d.2 . . 3  |-  ( ph  ->  B  =  C )
21adantr 463 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
32iuneq2dv 4293 1  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842   U_ciun 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-v 3061  df-in 3421  df-ss 3428  df-iun 4273
This theorem is referenced by:  iununi  4359  oelim2  7281  ituniiun  8834  dfrtrclrec2  13039  rtrclreclem1  13040  rtrclreclem2  13041  rtrclreclem4  13043  imasval  15125  mreacs  15272  cnextval  20853  taylfval  23046  iunpreima  27862  msubvrs  29772  trpredeq1  30034  trpredeq2  30035  neibastop2  30589  voliunnfl  31430  sstotbnd2  31552  equivtotbnd  31556  totbndbnd  31567  heiborlem3  31591  eliunov2  35658  fvmptiunrelexplb0d  35663  fvmptiunrelexplb1d  35665  comptiunov2i  35685  trclrelexplem  35690  dftrcl3  35699  trclfvcom  35702  cnvtrclfv  35703  cotrcltrcl  35704  trclimalb2  35705  trclfvdecomr  35707  dfrtrcl3  35712  dfrtrcl4  35717  otiunsndisjX  37934
  Copyright terms: Public domain W3C validator