Theorem iuneq2i 4980

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  dfiunv2  5002  iunrab  5019  iunidOLD  5028  iunin1  5039  2iunin  5043  resiun1  5973  resiun2  5974  dfimafn2  6927  dfmpt  7119  funiunfv  7225  fpar  8098  onovuni  8314  uniqs  8750  marypha2lem2  9394  alephlim  10027  cfsmolem  10230  ituniiun  10382  imasdsval2  17486  lpival  21241  pzriprnglem10  21407  pzriprnglem11  21408  cmpsublem  23293  txbasval  23500  uniioombllem2  25491  uniioombllem4  25494  volsup2  25513  itg1addlem5  25608  itg1climres  25622  indval2  32784  sigaclfu2  34118  measvuni  34211  fmla  35375  rabiun  37594  mblfinlem2  37659  voliunnfl  37665  cnambfre  37669  trclrelexplem  43707  cotrclrcl  43738  dfcoll2  44248  hoicvr  46553  hoidmv1le  46599  hoidmvle  46605  hspmbllem2  46632  smflimlem3  46778  smflimlem4  46779  smflim  46782  dfaimafn2  47171  xpiun  48150