Theorem iuneq2i 4973

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  dfiunv2  4992  iunrab  5011  iunin1  5030  2iunin  5036  resiun1  5992  resiun2  5993  dfimafn2  6942  dfmpt  7141  funiunfv  7246  fpar  8114  onovuni  8332  uniqs  8774  marypha2lem2  9407  alephlim  10071  cfsmolem  10273  ituniiun  10425  indval2  12248  imasdsval2  17603  lpival  21556  pzriprnglem10  21704  pzriprnglem11  21705  cmpsublem  23625  txbasval  23833  uniioombllem2  25812  uniioombllem4  25815  volsup2  25834  itg1addlem5  25929  itg1climres  25943  sigaclfu2  34632  measvuni  34726  fmla  35961  ttciun  37134  rabiun  38353  mblfinlem2  38408  voliunnfl  38414  cnambfre  38418  trclrelexplem  44552  cotrclrcl  44583  dfcoll2  45077  hoicvr  47377  hoidmv1le  47423  hoidmvle  47429  hspmbllem2  47456  smflimlem3  47602  smflimlem4  47603  smflim  47606  dfaimafn2  48055  xpiun  49075