Theorem iuneq2i 4989

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  dfiunv2  5011  iunrab  5028  iunidOLD  5037  iunin1  5048  2iunin  5052  resiun1  5986  resiun2  5987  dfimafn2  6942  dfmpt  7134  funiunfv  7240  fpar  8115  onovuni  8356  uniqs  8791  marypha2lem2  9448  alephlim  10081  cfsmolem  10284  ituniiun  10436  imasdsval2  17530  lpival  21285  pzriprnglem10  21451  pzriprnglem11  21452  cmpsublem  23337  txbasval  23544  uniioombllem2  25536  uniioombllem4  25539  volsup2  25558  itg1addlem5  25653  itg1climres  25667  indval2  32831  sigaclfu2  34152  measvuni  34245  fmla  35403  rabiun  37617  mblfinlem2  37682  voliunnfl  37688  cnambfre  37692  uniqsALTV  38347  trclrelexplem  43735  cotrclrcl  43766  dfcoll2  44276  hoicvr  46577  hoidmv1le  46623  hoidmvle  46629  hspmbllem2  46656  smflimlem3  46802  smflimlem4  46803  smflim  46806  dfaimafn2  47195  xpiun  48133