Theorem iuneq2i 5018

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-iun 4998

This theorem is referenced by:  dfiunv2  5040  iunrab  5057  iunidOLD  5066  iunin1  5077  2iunin  5081  resiun1  6020  resiun2  6021  dfimafn2  6972  dfmpt  7164  funiunfv  7268  fpar  8140  onovuni  8381  uniqs  8816  marypha2lem2  9474  alephlim  10105  cfsmolem  10308  ituniiun  10460  imasdsval2  17563  lpival  21352  pzriprnglem10  21519  pzriprnglem11  21520  cmpsublem  23423  txbasval  23630  uniioombllem2  25632  uniioombllem4  25635  volsup2  25654  itg1addlem5  25750  itg1climres  25764  indval2  33995  sigaclfu2  34102  measvuni  34195  fmla  35366  rabiun  37580  mblfinlem2  37645  voliunnfl  37651  cnambfre  37655  uniqsALTV  38311  trclrelexplem  43701  cotrclrcl  43732  dfcoll2  44248  hoicvr  46504  hoidmv1le  46550  hoidmvle  46556  hspmbllem2  46583  smflimlem3  46729  smflimlem4  46730  smflim  46733  dfaimafn2  47116  xpiun  48002