Theorem iuneq2i 4290

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

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   U_ciun 4272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-v 3073  df-in 3436  df-ss 3443  df-iun 4274

This theorem is referenced by:  dfiunv2  4307  iunrab  4318  iunid  4326  iunin1  4336  2iunin  4339  resiun1  5230  resiun2  5231  dfimafn2  5843  dfmpt  5989  funiunfv  6067  fpar  6779  onovuni  6906  uniqs  7263  marypha2lem2  7790  alephlim  8341  cfsmolem  8543  ituniiun  8695  imasdsval2  14565  lpival  17442  cmpsublem  19127  txbasval  19304  uniioombllem2  21189  uniioombllem4  21192  volsup2  21211  itg1addlem5  21304  itg1climres  21318  indval2  26609  sigaclfu2  26702  measvuni  26766  trpred0  27837  rabiun  28553  mblfinlem2  28570  voliunnfl  28576  cnambfre  28581  dfaimafn2  30213