Theorem iuneq2i 4982

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  dfiunv2  5002  iunrab  5021  iunin1  5040  2iunin  5046  resiun1  5999  resiun2  6000  dfimafn2  6945  dfmpt  7141  funiunfv  7247  fpar  8110  onovuni  8328  uniqs  8770  marypha2lem2  9395  alephlim  10050  cfsmolem  10253  ituniiun  10405  indval2  12222  imasdsval2  17569  lpival  21460  pzriprnglem10  21608  pzriprnglem11  21609  cmpsublem  23524  txbasval  23731  uniioombllem2  25710  uniioombllem4  25713  volsup2  25732  itg1addlem5  25827  itg1climres  25841  sigaclfu2  34455  measvuni  34548  fmla  35771  ttciun  36913  rabiun  38131  mblfinlem2  38196  voliunnfl  38202  cnambfre  38206  trclrelexplem  44328  cotrclrcl  44359  dfcoll2  44853  hoicvr  47153  hoidmv1le  47199  hoidmvle  47205  hspmbllem2  47232  smflimlem3  47378  smflimlem4  47379  smflim  47382  dfaimafn2  47791  xpiun  48811