Theorem iuneq2i 4971

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-v 3456  df-ss 3921  df-iun 4951

This theorem is referenced by:  dfiunv2  4991  iunrab  5010  iunin1  5029  2iunin  5033  resiun1  5985  resiun2  5986  dfimafn2  6930  dfmpt  7126  funiunfv  7232  fpar  8095  onovuni  8313  uniqs  8755  marypha2lem2  9382  alephlim  10023  cfsmolem  10227  ituniiun  10379  indval2  12200  imasdsval2  17546  lpival  21394  pzriprnglem10  21542  pzriprnglem11  21543  cmpsublem  23459  txbasval  23666  uniioombllem2  25645  uniioombllem4  25648  volsup2  25667  itg1addlem5  25762  itg1climres  25776  sigaclfu2  34418  measvuni  34511  fmla  35731  ttciun  36874  rabiun  38092  mblfinlem2  38157  voliunnfl  38163  cnambfre  38167  trclrelexplem  44287  cotrclrcl  44318  dfcoll2  44828  hoicvr  47122  hoidmv1le  47168  hoidmvle  47174  hspmbllem2  47201  smflimlem3  47347  smflimlem4  47348  smflim  47351  dfaimafn2  47760  xpiun  48780