Theorem iuneq2i 4961

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-ss 3914  df-iun 4941

This theorem is referenced by:  dfiunv2  4982  iunrab  4999  iunin1  5018  2iunin  5022  resiun1  5947  resiun2  5948  dfimafn2  6885  dfmpt  7077  funiunfv  7182  fpar  8046  onovuni  8262  uniqs  8698  marypha2lem2  9320  alephlim  9958  cfsmolem  10161  ituniiun  10313  imasdsval2  17420  lpival  21261  pzriprnglem10  21427  pzriprnglem11  21428  cmpsublem  23314  txbasval  23521  uniioombllem2  25511  uniioombllem4  25514  volsup2  25533  itg1addlem5  25628  itg1climres  25642  indval2  32835  sigaclfu2  34134  measvuni  34227  fmla  35425  rabiun  37643  mblfinlem2  37708  voliunnfl  37714  cnambfre  37718  trclrelexplem  43814  cotrclrcl  43845  dfcoll2  44355  hoicvr  46656  hoidmv1le  46702  hoidmvle  46708  hspmbllem2  46735  smflimlem3  46881  smflimlem4  46882  smflim  46885  dfaimafn2  47276  xpiun  48268