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

Theorem iuneq2d 4345
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 4340 1  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762   U_ciun 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-v 3108  df-in 3476  df-ss 3483  df-iun 4320
This theorem is referenced by:  iununi  4403  oelim2  7234  ituniiun  8791  imasval  14755  mreacs  14902  cnextval  20289  taylfval  22481  iunpreima  27091  dfrtrclrec2  28527  rtrclreclem.refl  28528  rtrclreclem.subset  28529  rtrclreclem.min  28531  trpredeq1  28866  trpredeq2  28867  voliunnfl  29622  neibastop2  29769  sstotbnd2  29860  equivtotbnd  29864  totbndbnd  29875  heiborlem3  29899  otiunsndisjX  31723
  Copyright terms: Public domain W3C validator