Theorem iuneq2i 4310

Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)

Hypothesis

Ref	Expression
iuneq2i.1	|- ( x e. A -> B = C )

Assertion

Ref	Expression
iuneq2i	|- U_ x e. A B = U_ x e. A C

Proof of Theorem iuneq2i

Step	Hyp	Ref	Expression
1		iuneq2 4308	. 2 |- ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )
2		iuneq2i.1	. 2 |- ( x e. A -> B = C )
3	1, 2	mprg 2762	1 |- U_ x e. A B = U_ x e. A C

Syntax hints:   -> wi 4   = wceq 1454   e. wcel 1897   U_ciun 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-v 3058  df-in 3422  df-ss 3429  df-iun 4293

This theorem is referenced by:  dfiunv2  4327  iunrab  4338  iunid  4346  iunin1  4356  2iunin  4359  resiun1  5141  resiun2  5142  dfimafn2  5937  dfmpt  6092  funiunfv  6177  fpar  6926  onovuni  7086  uniqs  7448  marypha2lem2  7975  alephlim  8523  cfsmolem  8725  ituniiun  8877  imasdsval2  15465  imasdsval2OLD  15477  lpival  18517  cmpsublem  20462  txbasval  20669  uniioombllem2  22588  uniioombllem2OLD  22589  uniioombllem4  22592  volsup2  22611  itg1addlem5  22706  itg1climres  22720  indval2  28884  sigaclfu2  28991  measvuni  29084  trpred0  30525  rabiun  31970  mblfinlem2  32022  voliunnfl  32028  cnambfre  32033  trclrelexplem  36347  cotrclrcl  36378  hoicvr  38407  hoidmv1le  38453  hoidmvle  38459  hspmbllem2  38486  dfaimafn2  38705  xpiun  40038