Theorem iuneq2i 4334

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

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804   U_ciun 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-v 3097  df-in 3468  df-ss 3475  df-iun 4317

This theorem is referenced by:  dfiunv2  4351  iunrab  4362  iunid  4370  iunin1  4380  2iunin  4383  resiun1  5282  resiun2  5283  dfimafn2  5908  dfmpt  6061  funiunfv  6145  fpar  6889  onovuni  7015  uniqs  7373  marypha2lem2  7898  alephlim  8451  cfsmolem  8653  ituniiun  8805  imasdsval2  14790  lpival  17767  cmpsublem  19772  txbasval  19980  uniioombllem2  21865  uniioombllem4  21868  volsup2  21887  itg1addlem5  21980  itg1climres  21994  indval2  27901  sigaclfu2  27994  measvuni  28058  trpred0  29294  rabiun  30011  mblfinlem2  30027  voliunnfl  30033  cnambfre  30038  dfaimafn2  32089  xpiun  32292