Theorem iuneq2i 4980

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  dfiunv2  5000  iunrab  5019  iunin1  5038  2iunin  5044  resiun1  6000  resiun2  6001  dfimafn2  6948  dfmpt  7146  funiunfv  7251  fpar  8117  onovuni  8335  uniqs  8777  marypha2lem2  9403  alephlim  10067  cfsmolem  10269  ituniiun  10421  indval2  12240  imasdsval2  17594  lpival  21544  pzriprnglem10  21692  pzriprnglem11  21693  cmpsublem  23608  txbasval  23816  uniioombllem2  25795  uniioombllem4  25798  volsup2  25817  itg1addlem5  25912  itg1climres  25926  sigaclfu2  34577  measvuni  34671  fmla  35912  ttciun  37084  rabiun  38303  mblfinlem2  38368  voliunnfl  38374  cnambfre  38378  trclrelexplem  44497  cotrclrcl  44528  dfcoll2  45022  hoicvr  47322  hoidmv1le  47368  hoidmvle  47374  hspmbllem2  47401  smflimlem3  47547  smflimlem4  47548  smflim  47551  dfaimafn2  47963  xpiun  48983