Theorem iuneq2i 4475

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457

This theorem is referenced by:  dfiunv2  4492  iunrab  4503  iunid  4511  iunin1  4521  2iunin  4524  resiun1  5336  resiun1OLD  5337  resiun2  5338  dfimafn2  6156  dfmpt  6316  funiunfv  6410  fpar  7168  onovuni  7326  uniqs  7694  marypha2lem2  8225  alephlim  8773  cfsmolem  8975  ituniiun  9127  imasdsval2  15999  lpival  19066  cmpsublem  21012  txbasval  21219  uniioombllem2  23157  uniioombllem4  23160  volsup2  23179  itg1addlem5  23273  itg1climres  23287  indval2  29404  sigaclfu2  29511  measvuni  29604  trpred0  30980  rabiun  32552  mblfinlem2  32617  voliunnfl  32623  cnambfre  32628  trclrelexplem  37022  cotrclrcl  37053  hoicvr  39438  hoidmv1le  39484  hoidmvle  39490  hspmbllem2  39517  smflimlem3  39659  smflimlem4  39660  smflim  39663  dfaimafn2  39895  xpiun  41556