Theorem iuneq2i 4989

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∪ ciun 4967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  dfiunv2  5011  iunrab  5028  iunidOLD  5037  iunin1  5048  2iunin  5052  resiun1  5986  resiun2  5987  dfimafn2  6941  dfmpt  7133  funiunfv  7239  fpar  8113  onovuni  8354  uniqs  8789  marypha2lem2  9446  alephlim  10079  cfsmolem  10282  ituniiun  10434  imasdsval2  17528  lpival  21283  pzriprnglem10  21449  pzriprnglem11  21450  cmpsublem  23335  txbasval  23542  uniioombllem2  25534  uniioombllem4  25537  volsup2  25556  itg1addlem5  25651  itg1climres  25665  indval2  32777  sigaclfu2  34098  measvuni  34191  fmla  35349  rabiun  37563  mblfinlem2  37628  voliunnfl  37634  cnambfre  37638  uniqsALTV  38293  trclrelexplem  43682  cotrclrcl  43713  dfcoll2  44224  hoicvr  46525  hoidmv1le  46571  hoidmvle  46577  hspmbllem2  46604  smflimlem3  46750  smflimlem4  46751  smflim  46754  dfaimafn2  47143  xpiun  48081