Theorem iuneq2i 5036

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  dfiunv2  5058  iunrab  5075  iunidOLD  5084  iunin1  5095  2iunin  5099  resiun1  6029  resiun2  6030  dfimafn2  6985  dfmpt  7178  funiunfv  7285  fpar  8157  onovuni  8398  uniqs  8835  marypha2lem2  9505  alephlim  10136  cfsmolem  10339  ituniiun  10491  imasdsval2  17576  lpival  21357  pzriprnglem10  21524  pzriprnglem11  21525  cmpsublem  23428  txbasval  23635  uniioombllem2  25637  uniioombllem4  25640  volsup2  25659  itg1addlem5  25755  itg1climres  25769  indval2  33978  sigaclfu2  34085  measvuni  34178  fmla  35349  rabiun  37553  mblfinlem2  37618  voliunnfl  37624  cnambfre  37628  uniqsALTV  38285  trclrelexplem  43673  cotrclrcl  43704  dfcoll2  44221  hoicvr  46469  hoidmv1le  46515  hoidmvle  46521  hspmbllem2  46548  smflimlem3  46694  smflimlem4  46695  smflim  46698  dfaimafn2  47081  xpiun  47881