Theorem iuneq2i 4539

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

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-iun 4522

This theorem is referenced by:  dfiunv2  4556  iunrab  4567  iunid  4575  iunin1  4585  2iunin  4588  resiun1  5416  resiun1OLD  5417  resiun2  5418  dfimafn2  6246  dfmpt  6410  funiunfv  6506  fpar  7281  onovuni  7439  uniqs  7807  marypha2lem2  8342  alephlim  8890  cfsmolem  9092  ituniiun  9244  imasdsval2  16176  lpival  19245  cmpsublem  21202  txbasval  21409  uniioombllem2  23351  uniioombllem4  23354  volsup2  23373  itg1addlem5  23467  itg1climres  23481  indval2  30076  sigaclfu2  30184  measvuni  30277  trpred0  31736  rabiun  33382  mblfinlem2  33447  voliunnfl  33453  cnambfre  33458  uniqsALTV  34101  trclrelexplem  38003  cotrclrcl  38034  hoicvr  40762  hoidmv1le  40808  hoidmvle  40814  hspmbllem2  40841  smflimlem3  40981  smflimlem4  40982  smflim  40985  dfaimafn2  41246  xpiun  41766