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

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

Proof of Theorem iuneq2d
StepHypRef Expression
1 iuneq2d.2 . . 3 (𝜑𝐵 = 𝐶)
21adantr 479 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32iuneq2dv 4469 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976   ciun 4446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-v 3171  df-in 3543  df-ss 3550  df-iun 4448
This theorem is referenced by:  iununi  4537  oelim2  7536  ituniiun  9101  dfrtrclrec2  13588  rtrclreclem1  13589  rtrclreclem2  13590  rtrclreclem4  13592  imasval  15937  mreacs  16085  cnextval  21614  taylfval  23831  iunpreima  28568  msubvrs  30514  trpredeq1  30767  trpredeq2  30768  neibastop2  31329  voliunnfl  32423  sstotbnd2  32543  equivtotbnd  32547  totbndbnd  32558  heiborlem3  32582  eliunov2  36790  fvmptiunrelexplb0d  36795  fvmptiunrelexplb1d  36797  comptiunov2i  36817  trclrelexplem  36822  dftrcl3  36831  trclfvcom  36834  cnvtrclfv  36835  cotrcltrcl  36836  trclimalb2  36837  trclfvdecomr  36839  dfrtrcl3  36844  dfrtrcl4  36849  isomenndlem  39221  ovnval  39232  hoicvr  39239  hoicvrrex  39247  ovnlecvr  39249  ovncvrrp  39255  ovnsubaddlem1  39261  hoidmvlelem3  39288  hoidmvle  39291  ovnhoilem1  39292  ovnovollem1  39347  smflimlem3  39460  otiunsndisjX  40129
  Copyright terms: Public domain W3C validator