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

Theorem iuneq2d 5022
Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
Hypothesis
Ref Expression
iuneq2d.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
iuneq2d (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2d
StepHypRef Expression
1 iuneq2d.2 . . 3 (𝜑𝐵 = 𝐶)
21adantr 480 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32iuneq2dv 5016 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993
This theorem is referenced by:  iununi  5099  oelim2  8633  ituniiun  10462  rtrclreclem1  15096  dfrtrclrec2  15097  rtrclreclem2  15098  rtrclreclem4  15100  imasval  17556  mreacs  17701  pzriprnglem10  21501  cnextval  24069  taylfval  26400  iunpreima  32577  constrlim  33780  reprdifc  34642  msubvrs  35565  neibastop2  36362  voliunnfl  37671  sstotbnd2  37781  equivtotbnd  37785  totbndbnd  37796  heiborlem3  37820  eliunov2  43692  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  comptiunov2i  43719  trclrelexplem  43724  dftrcl3  43733  trclfvcom  43736  cnvtrclfv  43737  cotrcltrcl  43738  trclimalb2  43739  trclfvdecomr  43741  dfrtrcl3  43746  dfrtrcl4  43751  isomenndlem  46545  ovnval  46556  hoicvr  46563  hoicvrrex  46571  ovnlecvr  46573  ovncvrrp  46579  ovnsubaddlem1  46585  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem1  46616  ovnovollem1  46671  smflimlem3  46788  otiunsndisjX  47291
  Copyright terms: Public domain W3C validator