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

Theorem iuneq2d 4939
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 481 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32iuneq2dv 4934 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105   ciun 4910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-v 3494  df-in 3940  df-ss 3949  df-iun 4912
This theorem is referenced by:  iununi  5012  oelim2  8210  ituniiun  9832  dfrtrclrec2  14404  rtrclreclem1  14405  rtrclreclem2  14406  rtrclreclem4  14408  imasval  16772  mreacs  16917  cnextval  22597  taylfval  24874  iunpreima  30244  reprdifc  31797  msubvrs  32704  trpredeq1  32956  trpredeq2  32957  neibastop2  33606  voliunnfl  34817  sstotbnd2  34933  equivtotbnd  34937  totbndbnd  34948  heiborlem3  34972  eliunov2  39902  fvmptiunrelexplb0d  39907  fvmptiunrelexplb1d  39909  comptiunov2i  39929  trclrelexplem  39934  dftrcl3  39943  trclfvcom  39946  cnvtrclfv  39947  cotrcltrcl  39948  trclimalb2  39949  trclfvdecomr  39951  dfrtrcl3  39956  dfrtrcl4  39961  isomenndlem  42689  ovnval  42700  hoicvr  42707  hoicvrrex  42715  ovnlecvr  42717  ovncvrrp  42723  ovnsubaddlem1  42729  hoidmvlelem3  42756  hoidmvle  42759  ovnhoilem1  42760  ovnovollem1  42815  smflimlem3  42926  otiunsndisjX  43355
  Copyright terms: Public domain W3C validator