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

Theorem iuneq2i 4915
 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 4913 . 2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
2 iuneq2i.1 . 2 (𝑥𝐴𝐵 = 𝐶)
31, 2mprg 3144 1 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2114  ∪ ciun 4894 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 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 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-in 3915  df-ss 3925  df-iun 4896 This theorem is referenced by:  dfiunv2  4935  iunrab  4951  iunid  4959  iunin1  4969  2iunin  4973  resiun1  5851  resiun2  5852  dfimafn2  6711  dfmpt  6888  funiunfv  6990  fpar  7798  onovuni  7966  uniqs  8344  marypha2lem2  8888  alephlim  9482  cfsmolem  9681  ituniiun  9833  imasdsval2  16780  lpival  20009  cmpsublem  22002  txbasval  22209  uniioombllem2  24185  uniioombllem4  24188  volsup2  24207  itg1addlem5  24302  itg1climres  24316  indval2  31347  sigaclfu2  31454  measvuni  31547  fmla  32702  trpred0  33149  rabiun  34992  mblfinlem2  35057  voliunnfl  35063  cnambfre  35067  uniqsALTV  35708  trclrelexplem  40346  cotrclrcl  40377  dfcoll2  40898  hoicvr  43130  hoidmv1le  43176  hoidmvle  43182  hspmbllem2  43209  smflimlem3  43349  smflimlem4  43350  smflim  43353  dfaimafn2  43665  xpiun  44329
 Copyright terms: Public domain W3C validator