Theorem iuneq2i 4942

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-in 3890  df-ss 3900  df-iun 4923

This theorem is referenced by:  dfiunv2  4961  iunrab  4978  iunid  4986  iunin1  4997  2iunin  5001  resiun1  5900  resiun2  5901  dfimafn2  6815  dfmpt  6998  funiunfv  7103  fpar  7927  onovuni  8144  uniqs  8524  marypha2lem2  9125  trpred0  9410  alephlim  9754  cfsmolem  9957  ituniiun  10109  imasdsval2  17144  lpival  20429  cmpsublem  22458  txbasval  22665  uniioombllem2  24652  uniioombllem4  24655  volsup2  24674  itg1addlem5  24770  itg1climres  24784  indval2  31882  sigaclfu2  31989  measvuni  32082  fmla  33243  rabiun  35677  mblfinlem2  35742  voliunnfl  35748  cnambfre  35752  uniqsALTV  36391  trclrelexplem  41208  cotrclrcl  41239  dfcoll2  41759  hoicvr  43976  hoidmv1le  44022  hoidmvle  44028  hspmbllem2  44055  smflimlem3  44195  smflimlem4  44196  smflim  44199  dfaimafn2  44545  xpiun  45208