Theorem iuneq2i 4262

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 4260	. 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 2745	1 |- U_ x e. A B = U_ x e. A C

Syntax hints:   -> wi 4   = wceq 1399   e. wcel 1826   U_ciun 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738  df-v 3036  df-in 3396  df-ss 3403  df-iun 4245

This theorem is referenced by:  dfiunv2  4279  iunrab  4290  iunid  4298  iunin1  4308  2iunin  4311  resiun1  5204  resiun2  5205  dfimafn2  5824  dfmpt  5978  funiunfv  6061  fpar  6803  onovuni  6931  uniqs  7289  marypha2lem2  7811  alephlim  8361  cfsmolem  8563  ituniiun  8715  imasdsval2  14923  lpival  18006  cmpsublem  19985  txbasval  20192  uniioombllem2  22077  uniioombllem4  22080  volsup2  22099  itg1addlem5  22192  itg1climres  22206  indval2  28163  sigaclfu2  28270  measvuni  28341  trpred0  29484  rabiun  30201  mblfinlem2  30217  voliunnfl  30223  cnambfre  30228  dfaimafn2  32417  xpiun  32772  trclrelexplem  38247  cotrclrcl  38250