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

Theorem iuneq2i 4683
Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
Hypothesis
Ref Expression
iuneq2i.1 (𝑥𝐴𝐵 = 𝐶)
Assertion
Ref Expression
iuneq2i 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶

Proof of Theorem iuneq2i
StepHypRef Expression
1 iuneq2 4681 . 2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
2 iuneq2i.1 . 2 (𝑥𝐴𝐵 = 𝐶)
31, 2mprg 3056 1 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  wcel 2131   ciun 4664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-v 3334  df-in 3714  df-ss 3721  df-iun 4666
This theorem is referenced by:  dfiunv2  4700  iunrab  4711  iunid  4719  iunin1  4729  2iunin  4732  resiun1  5566  resiun1OLD  5567  resiun2  5568  dfimafn2  6400  dfmpt  6565  funiunfv  6661  fpar  7441  onovuni  7600  uniqs  7966  marypha2lem2  8499  alephlim  9072  cfsmolem  9276  ituniiun  9428  imasdsval2  16370  lpival  19439  cmpsublem  21396  txbasval  21603  uniioombllem2  23543  uniioombllem4  23546  volsup2  23565  itg1addlem5  23658  itg1climres  23672  indval2  30377  sigaclfu2  30485  measvuni  30578  trpred0  32033  rabiun  33687  mblfinlem2  33752  voliunnfl  33758  cnambfre  33763  uniqsALTV  34417  trclrelexplem  38497  cotrclrcl  38528  hoicvr  41260  hoidmv1le  41306  hoidmvle  41312  hspmbllem2  41339  smflimlem3  41479  smflimlem4  41480  smflim  41483  dfaimafn2  41744  xpiun  42268
  Copyright terms: Public domain W3C validator