Theorem iuneq2i 4943

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4923

This theorem is referenced by:  dfiunv2  4963  iunrab  4982  iunin1  5001  2iunin  5005  resiun1  5951  resiun2  5952  dfimafn2  6890  dfmpt  7086  funiunfv  7192  fpar  8055  onovuni  8272  uniqs  8710  marypha2lem2  9339  alephlim  9980  cfsmolem  10183  ituniiun  10335  indval2  12155  imasdsval2  17471  lpival  21317  pzriprnglem10  21465  pzriprnglem11  21466  cmpsublem  23382  txbasval  23589  uniioombllem2  25568  uniioombllem4  25571  volsup2  25590  itg1addlem5  25685  itg1climres  25699  sigaclfu2  34305  measvuni  34398  fmla  35609  ttciun  36742  rabiun  37960  mblfinlem2  38025  voliunnfl  38031  cnambfre  38035  trclrelexplem  44155  cotrclrcl  44186  dfcoll2  44696  hoicvr  46991  hoidmv1le  47037  hoidmvle  47043  hspmbllem2  47070  smflimlem3  47216  smflimlem4  47217  smflim  47220  dfaimafn2  47629  xpiun  48649