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

Theorem iuneq2i 4931
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 4929 . 2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
2 iuneq2i.1 . 2 (𝑥𝐴𝐵 = 𝐶)
31, 2mprg 3149 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:  dfiunv2  4951  iunrab  4967  iunid  4975  iunin1  4985  2iunin  4989  resiun1  5866  resiun2  5867  dfimafn2  6722  dfmpt  6898  funiunfv  6998  fpar  7800  onovuni  7968  uniqs  8346  marypha2lem2  8888  alephlim  9481  cfsmolem  9680  ituniiun  9832  imasdsval2  16777  lpival  19946  cmpsublem  21935  txbasval  22142  uniioombllem2  24111  uniioombllem4  24114  volsup2  24133  itg1addlem5  24228  itg1climres  24242  indval2  31172  sigaclfu2  31279  measvuni  31372  fmla  32525  trpred0  32972  rabiun  34746  mblfinlem2  34811  voliunnfl  34817  cnambfre  34821  uniqsALTV  35467  trclrelexplem  39934  cotrclrcl  39965  dfcoll2  40465  hoicvr  42707  hoidmv1le  42753  hoidmvle  42759  hspmbllem2  42786  smflimlem3  42926  smflimlem4  42927  smflim  42930  dfaimafn2  43242  xpiun  43910
  Copyright terms: Public domain W3C validator