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

Theorem iuneq2i 4507
 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 4505 . 2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
2 iuneq2i.1 . 2 (𝑥𝐴𝐵 = 𝐶)
31, 2mprg 2921 1 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987  ∪ ciun 4487 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3188  df-in 3563  df-ss 3570  df-iun 4489 This theorem is referenced by:  dfiunv2  4524  iunrab  4535  iunid  4543  iunin1  4553  2iunin  4556  resiun1  5377  resiun1OLD  5378  resiun2  5379  dfimafn2  6205  dfmpt  6367  funiunfv  6463  fpar  7229  onovuni  7387  uniqs  7755  marypha2lem2  8289  alephlim  8837  cfsmolem  9039  ituniiun  9191  imasdsval2  16100  lpival  19167  cmpsublem  21115  txbasval  21322  uniioombllem2  23264  uniioombllem4  23267  volsup2  23286  itg1addlem5  23380  itg1climres  23394  indval2  29870  sigaclfu2  29977  measvuni  30070  trpred0  31458  rabiun  33035  mblfinlem2  33100  voliunnfl  33106  cnambfre  33111  trclrelexplem  37505  cotrclrcl  37536  hoicvr  40085  hoidmv1le  40131  hoidmvle  40137  hspmbllem2  40164  smflimlem3  40304  smflimlem4  40305  smflim  40308  dfaimafn2  40566  xpiun  41070
 Copyright terms: Public domain W3C validator