Theorem iuneq2i 4951

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  ∪ ciun 4930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-v 3433  df-in 3899  df-ss 3909  df-iun 4932

This theorem is referenced by:  dfiunv2  4970  iunrab  4987  iunid  4995  iunin1  5006  2iunin  5010  resiun1  5910  resiun2  5911  dfimafn2  6830  dfmpt  7013  funiunfv  7118  fpar  7948  onovuni  8165  uniqs  8558  marypha2lem2  9183  trpred0  9489  alephlim  9834  cfsmolem  10037  ituniiun  10189  imasdsval2  17238  lpival  20527  cmpsublem  22561  txbasval  22768  uniioombllem2  24758  uniioombllem4  24761  volsup2  24780  itg1addlem5  24876  itg1climres  24890  indval2  31991  sigaclfu2  32098  measvuni  32191  fmla  33352  rabiun  35759  mblfinlem2  35824  voliunnfl  35830  cnambfre  35834  uniqsALTV  36473  trclrelexplem  41301  cotrclrcl  41332  dfcoll2  41852  hoicvr  44068  hoidmv1le  44114  hoidmvle  44120  hspmbllem2  44147  smflimlem3  44287  smflimlem4  44288  smflim  44291  dfaimafn2  44637  xpiun  45299