Theorem iuneq2i 4966

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∪ ciun 4944

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-v 3440  df-ss 3916  df-iun 4946

This theorem is referenced by:  dfiunv2  4987  iunrab  5006  iunin1  5025  2iunin  5029  resiun1  5956  resiun2  5957  dfimafn2  6895  dfmpt  7087  funiunfv  7192  fpar  8056  onovuni  8272  uniqs  8709  marypha2lem2  9337  alephlim  9975  cfsmolem  10178  ituniiun  10330  imasdsval2  17435  lpival  21277  pzriprnglem10  21443  pzriprnglem11  21444  cmpsublem  23341  txbasval  23548  uniioombllem2  25538  uniioombllem4  25541  volsup2  25560  itg1addlem5  25655  itg1climres  25669  indval2  32882  sigaclfu2  34227  measvuni  34320  fmla  35524  rabiun  37733  mblfinlem2  37798  voliunnfl  37804  cnambfre  37808  trclrelexplem  43894  cotrclrcl  43925  dfcoll2  44435  hoicvr  46734  hoidmv1le  46780  hoidmvle  46786  hspmbllem2  46813  smflimlem3  46959  smflimlem4  46960  smflim  46963  dfaimafn2  47354  xpiun  48346