Theorem iuneq2i 4970

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  dfiunv2  4991  iunrab  5010  iunin1  5029  2iunin  5033  resiun1  5966  resiun2  5967  dfimafn2  6905  dfmpt  7099  funiunfv  7204  fpar  8068  onovuni  8284  uniqs  8722  marypha2lem2  9351  alephlim  9989  cfsmolem  10192  ituniiun  10344  imasdsval2  17449  lpival  21291  pzriprnglem10  21457  pzriprnglem11  21458  cmpsublem  23355  txbasval  23562  uniioombllem2  25552  uniioombllem4  25555  volsup2  25574  itg1addlem5  25669  itg1climres  25683  indval2  32944  sigaclfu2  34299  measvuni  34392  fmla  35597  rabiun  37844  mblfinlem2  37909  voliunnfl  37915  cnambfre  37919  trclrelexplem  44067  cotrclrcl  44098  dfcoll2  44608  hoicvr  46906  hoidmv1le  46952  hoidmvle  46958  hspmbllem2  46985  smflimlem3  47131  smflimlem4  47132  smflim  47135  dfaimafn2  47526  xpiun  48518