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

Theorem iuneq2d 4218
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 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
32iuneq2dv 4213 1  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   U_ciun 4192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741  df-rex 2742  df-v 2995  df-in 3356  df-ss 3363  df-iun 4194
This theorem is referenced by:  iununi  4276  oelim2  7055  ituniiun  8612  imasval  14470  mreacs  14617  cnextval  19655  taylfval  21846  iunpreima  25937  dfrtrclrec2  27367  rtrclreclem.refl  27368  rtrclreclem.subset  27369  rtrclreclem.min  27371  trpredeq1  27706  trpredeq2  27707  voliunnfl  28461  neibastop2  28608  sstotbnd2  28699  equivtotbnd  28703  totbndbnd  28714  heiborlem3  28738  otiunsndisjX  30159
  Copyright terms: Public domain W3C validator