Theorem iuneq2i 4972

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3897  df-iun 4952

This theorem is used by:  dfiunv2  4991  iunrab  5010  iunin1  5029  2iunin  5035  resiun1  5991  resiun2  5992  dfimafn2  6953  dfmpt  7152  funiunfv  7256  fpar  8134  onovuni  8358  uniqs  8802  marypha2lem2  9435  alephlim  10153  cfsmolem  10355  ituniiun  10507  indval2  12332  imasdsval2  17697  lpival  21657  pzriprnglem10  21805  pzriprnglem11  21806  cmpsublem  23726  txbasval  23934  uniioombllem2  25913  uniioombllem4  25916  volsup2  25935  itg1addlem5  26030  itg1climres  26044  sigaclfu2  34803  measvuni  34897  fmla  36264  ttciun  37426  rabiun  38658  mblfinlem2  38713  voliunnfl  38719  cnambfre  38723  trclrelexplem  44848  cotrclrcl  44879  dfcoll2  45373  hoicvr  47694  hoidmv1le  47740  hoidmvle  47746  hspmbllem2  47773  smflimlem3  47919  smflimlem4  47920  smflim  47923  dfaimafn2  48372  xpiun  49392