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

Theorem iuneq2d 4921
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 484 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32iuneq2dv 4916 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115   ciun 4892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-v 3473  df-in 3917  df-ss 3927  df-iun 4894
This theorem is referenced by:  iununi  4994  oelim2  8196  ituniiun  9821  dfrtrclrec2  14395  rtrclreclem1  14396  rtrclreclem2  14397  rtrclreclem4  14399  imasval  16763  mreacs  16908  cnextval  22645  taylfval  24933  iunpreima  30303  reprdifc  31906  msubvrs  32815  trpredeq1  33067  trpredeq2  33068  neibastop2  33717  voliunnfl  34987  sstotbnd2  35098  equivtotbnd  35102  totbndbnd  35113  heiborlem3  35137  eliunov2  40191  fvmptiunrelexplb0d  40196  fvmptiunrelexplb1d  40198  comptiunov2i  40218  trclrelexplem  40223  dftrcl3  40232  trclfvcom  40235  cnvtrclfv  40236  cotrcltrcl  40237  trclimalb2  40238  trclfvdecomr  40240  dfrtrcl3  40245  dfrtrcl4  40250  isomenndlem  42992  ovnval  43003  hoicvr  43010  hoicvrrex  43018  ovnlecvr  43020  ovncvrrp  43026  ovnsubaddlem1  43032  hoidmvlelem3  43059  hoidmvle  43062  ovnhoilem1  43063  ovnovollem1  43118  smflimlem3  43229  otiunsndisjX  43658
  Copyright terms: Public domain W3C validator