Theorem iuneq2i 4973

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

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

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 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  dfiunv2  4994  iunrab  5011  iunidOLD  5020  iunin1  5031  2iunin  5035  resiun1  5959  resiun2  5960  dfimafn2  6906  dfmpt  7098  funiunfv  7204  fpar  8072  onovuni  8288  uniqs  8724  marypha2lem2  9363  alephlim  9996  cfsmolem  10199  ituniiun  10351  imasdsval2  17455  lpival  21266  pzriprnglem10  21432  pzriprnglem11  21433  cmpsublem  23319  txbasval  23526  uniioombllem2  25517  uniioombllem4  25520  volsup2  25539  itg1addlem5  25634  itg1climres  25648  indval2  32827  sigaclfu2  34104  measvuni  34197  fmla  35361  rabiun  37580  mblfinlem2  37645  voliunnfl  37651  cnambfre  37655  trclrelexplem  43693  cotrclrcl  43724  dfcoll2  44234  hoicvr  46539  hoidmv1le  46585  hoidmvle  46591  hspmbllem2  46618  smflimlem3  46764  smflimlem4  46765  smflim  46768  dfaimafn2  47160  xpiun  48139