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 3067	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∪ ciun 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-v 3476  df-in 3955  df-ss 3965  df-iun 4999

This theorem is referenced by:  dfiunv2  5038  iunrab  5055  iunidOLD  5064  iunin1  5075  2iunin  5079  resiun1  6001  resiun2  6002  dfimafn2  6955  dfmpt  7144  funiunfv  7249  fpar  8104  onovuni  8344  uniqs  8773  marypha2lem2  9433  alephlim  10064  cfsmolem  10267  ituniiun  10419  imasdsval2  17466  lpival  21083  pzriprnglem10  21259  pzriprnglem11  21260  cmpsublem  23123  txbasval  23330  uniioombllem2  25324  uniioombllem4  25327  volsup2  25346  itg1addlem5  25442  itg1climres  25456  indval2  33298  sigaclfu2  33405  measvuni  33498  fmla  34658  rabiun  36764  mblfinlem2  36829  voliunnfl  36835  cnambfre  36839  uniqsALTV  37501  trclrelexplem  42764  cotrclrcl  42795  dfcoll2  43313  hoicvr  45563  hoidmv1le  45609  hoidmvle  45615  hspmbllem2  45642  smflimlem3  45788  smflimlem4  45789  smflim  45792  dfaimafn2  46173  xpiun  46835