Theorem iuneq2i 5013

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  dfiunv2  5035  iunrab  5052  iunidOLD  5061  iunin1  5072  2iunin  5076  resiun1  6017  resiun2  6018  dfimafn2  6972  dfmpt  7164  funiunfv  7268  fpar  8141  onovuni  8382  uniqs  8817  marypha2lem2  9476  alephlim  10107  cfsmolem  10310  ituniiun  10462  imasdsval2  17561  lpival  21334  pzriprnglem10  21501  pzriprnglem11  21502  cmpsublem  23407  txbasval  23614  uniioombllem2  25618  uniioombllem4  25621  volsup2  25640  itg1addlem5  25735  itg1climres  25749  indval2  32839  sigaclfu2  34122  measvuni  34215  fmla  35386  rabiun  37600  mblfinlem2  37665  voliunnfl  37671  cnambfre  37675  uniqsALTV  38330  trclrelexplem  43724  cotrclrcl  43755  dfcoll2  44271  hoicvr  46563  hoidmv1le  46609  hoidmvle  46615  hspmbllem2  46642  smflimlem3  46788  smflimlem4  46789  smflim  46792  dfaimafn2  47178  xpiun  48074