Theorem iuneq2i 4963

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 4961	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
2		iuneq2i.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
3	1, 2	mprg 3050	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶

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

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 3438  df-ss 3920  df-iun 4943

This theorem is referenced by:  dfiunv2  4984  iunrab  5001  iunidOLD  5010  iunin1  5021  2iunin  5025  resiun1  5950  resiun2  5951  dfimafn2  6886  dfmpt  7078  funiunfv  7184  fpar  8049  onovuni  8265  uniqs  8701  marypha2lem2  9326  alephlim  9961  cfsmolem  10164  ituniiun  10316  imasdsval2  17420  lpival  21231  pzriprnglem10  21397  pzriprnglem11  21398  cmpsublem  23284  txbasval  23491  uniioombllem2  25482  uniioombllem4  25485  volsup2  25504  itg1addlem5  25599  itg1climres  25613  indval2  32797  sigaclfu2  34088  measvuni  34181  fmla  35358  rabiun  37577  mblfinlem2  37642  voliunnfl  37648  cnambfre  37652  trclrelexplem  43688  cotrclrcl  43719  dfcoll2  44229  hoicvr  46533  hoidmv1le  46579  hoidmvle  46585  hspmbllem2  46612  smflimlem3  46758  smflimlem4  46759  smflim  46762  dfaimafn2  47154  xpiun  48146