Theorem iuneq2i 4978

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4958

This theorem is used by:  dfiunv2  4997  iunrab  5016  iunin1  5035  2iunin  5041  resiun1  6006  resiun2  6007  dfimafn2  6979  dfmpt  7179  funiunfv  7283  fpar  8164  onovuni  8388  uniqs  8832  marypha2lem2  9465  alephlim  10185  cfsmolem  10387  ituniiun  10539  indval2  12365  imasdsval2  17738  lpival  21699  pzriprnglem10  21851  pzriprnglem11  21852  cmpsublem  23772  txbasval  23980  uniioombllem2  25959  uniioombllem4  25962  volsup2  25981  itg1addlem5  26076  itg1climres  26090  sigaclfu2  34864  measvuni  34958  fmla  36354  ttciun  37517  rabiun  38789  mblfinlem2  38844  voliunnfl  38850  cnambfre  38854  trclrelexplem  44972  cotrclrcl  45003  dfcoll2  45497  hoicvr  47831  hoidmv1le  47877  hoidmvle  47883  hspmbllem2  47910  smflimlem3  48056  smflimlem4  48057  smflim  48060  dfaimafn2  48509  xpiun  49529