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

Theorem iuneq2d 4264
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 466 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
32iuneq2dv 4259 1  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872   U_ciun 4237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ral 2714  df-rex 2715  df-v 3019  df-in 3381  df-ss 3388  df-iun 4239
This theorem is referenced by:  iununi  4325  oelim2  7246  ituniiun  8798  dfrtrclrec2  13059  rtrclreclem1  13060  rtrclreclem2  13061  rtrclreclem4  13063  imasval  15349  imasvalOLD  15350  mreacs  15502  cnextval  21013  taylfval  23251  iunpreima  28121  msubvrs  30145  trpredeq1  30407  trpredeq2  30408  neibastop2  30961  voliunnfl  31891  sstotbnd2  32013  equivtotbnd  32017  totbndbnd  32028  heiborlem3  32052  eliunov2  36184  fvmptiunrelexplb0d  36189  fvmptiunrelexplb1d  36191  comptiunov2i  36211  trclrelexplem  36216  dftrcl3  36225  trclfvcom  36228  cnvtrclfv  36229  cotrcltrcl  36230  trclimalb2  36231  trclfvdecomr  36233  dfrtrcl3  36238  dfrtrcl4  36243  isomenndlem  38202  ovnval  38209  hoicvr  38217  hoicvrrex  38225  ovnlecvr  38227  ovncvrrp  38233  ovnsubaddlem1  38239  hoidmvlelem3  38266  hoidmvle  38269  ovnhoilem1  38270  otiunsndisjX  38814
  Copyright terms: Public domain W3C validator