Theorem iuneq2i 4261

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

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1872   U_ciun 4242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720  df-v 3024  df-in 3386  df-ss 3393  df-iun 4244

This theorem is referenced by:  dfiunv2  4278  iunrab  4289  iunid  4297  iunin1  4307  2iunin  4310  resiun1  5085  resiun2  5086  dfimafn2  5875  dfmpt  6028  funiunfv  6112  fpar  6855  onovuni  7016  uniqs  7378  marypha2lem2  7903  alephlim  8449  cfsmolem  8651  ituniiun  8803  imasdsval2  15360  imasdsval2OLD  15372  lpival  18412  cmpsublem  20356  txbasval  20563  uniioombllem2  22482  uniioombllem2OLD  22483  uniioombllem4  22486  volsup2  22505  itg1addlem5  22600  itg1climres  22614  indval2  28788  sigaclfu2  28895  measvuni  28988  trpred0  30428  rabiun  31833  mblfinlem2  31885  voliunnfl  31891  cnambfre  31896  trclrelexplem  36216  cotrclrcl  36247  hoicvr  38217  hoidmv1le  38263  hoidmvle  38269  dfaimafn2  38481  xpiun  39367