Theorem iuneq2i 4344

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   U_ciun 4325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327

This theorem is referenced by:  dfiunv2  4361  iunrab  4372  iunid  4380  iunin1  4390  2iunin  4393  resiun1  5290  resiun2  5291  dfimafn2  5915  dfmpt  6064  funiunfv  6146  fpar  6884  onovuni  7010  uniqs  7368  marypha2lem2  7892  alephlim  8444  cfsmolem  8646  ituniiun  8798  imasdsval2  14767  lpival  17675  cmpsublem  19665  txbasval  19842  uniioombllem2  21727  uniioombllem4  21730  volsup2  21749  itg1addlem5  21842  itg1climres  21856  indval2  27668  sigaclfu2  27761  measvuni  27825  trpred0  28896  rabiun  29613  mblfinlem2  29629  voliunnfl  29635  cnambfre  29640  dfaimafn2  31718