Theorem iuneq2i 4977

Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)

Hypothesis

Ref	Expression
iuneq2i.1	⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶

Proof of Theorem iuneq2i

Step	Hyp	Ref	Expression
1		iuneq2 4975	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
2		iuneq2i.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
3	1, 2	mprg 3050	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  dfiunv2  4999  iunrab  5016  iunidOLD  5025  iunin1  5036  2iunin  5040  resiun1  5970  resiun2  5971  dfimafn2  6924  dfmpt  7116  funiunfv  7222  fpar  8095  onovuni  8311  uniqs  8747  marypha2lem2  9387  alephlim  10020  cfsmolem  10223  ituniiun  10375  imasdsval2  17479  lpival  21234  pzriprnglem10  21400  pzriprnglem11  21401  cmpsublem  23286  txbasval  23493  uniioombllem2  25484  uniioombllem4  25487  volsup2  25506  itg1addlem5  25601  itg1climres  25615  indval2  32777  sigaclfu2  34111  measvuni  34204  fmla  35368  rabiun  37587  mblfinlem2  37652  voliunnfl  37658  cnambfre  37662  trclrelexplem  43700  cotrclrcl  43731  dfcoll2  44241  hoicvr  46546  hoidmv1le  46592  hoidmvle  46598  hspmbllem2  46625  smflimlem3  46771  smflimlem4  46772  smflim  46775  dfaimafn2  47167  xpiun  48146