Theorem iuneq2i 4731

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

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2156  ∪ ciun 4712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-v 3393  df-in 3776  df-ss 3783  df-iun 4714

This theorem is referenced by:  dfiunv2  4748  iunrab  4759  iunid  4767  iunin1  4777  2iunin  4780  resiun1  5620  resiun2  5621  dfimafn2  6463  dfmpt  6629  funiunfv  6726  fpar  7511  onovuni  7671  uniqs  8038  marypha2lem2  8577  alephlim  9169  cfsmolem  9373  ituniiun  9525  imasdsval2  16377  lpival  19450  cmpsublem  21413  txbasval  21620  uniioombllem2  23563  uniioombllem4  23566  volsup2  23585  itg1addlem5  23680  itg1climres  23694  indval2  30400  sigaclfu2  30508  measvuni  30601  trpred0  32054  rabiun  33693  mblfinlem2  33758  voliunnfl  33764  cnambfre  33768  uniqsALTV  34414  trclrelexplem  38500  cotrclrcl  38531  hoicvr  41241  hoidmv1le  41287  hoidmvle  41293  hspmbllem2  41320  smflimlem3  41460  smflimlem4  41461  smflim  41464  dfaimafn2  41752  xpiun  42331