Theorem iuneq2i 4968

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-iun 4948

This theorem is referenced by:  dfiunv2  4989  iunrab  5008  iunin1  5027  2iunin  5031  resiun1  5958  resiun2  5959  dfimafn2  6897  dfmpt  7089  funiunfv  7194  fpar  8058  onovuni  8274  uniqs  8711  marypha2lem2  9339  alephlim  9977  cfsmolem  10180  ituniiun  10332  imasdsval2  17437  lpival  21279  pzriprnglem10  21445  pzriprnglem11  21446  cmpsublem  23343  txbasval  23550  uniioombllem2  25540  uniioombllem4  25543  volsup2  25562  itg1addlem5  25657  itg1climres  25671  indval2  32933  sigaclfu2  34278  measvuni  34371  fmla  35575  rabiun  37794  mblfinlem2  37859  voliunnfl  37865  cnambfre  37869  trclrelexplem  43952  cotrclrcl  43983  dfcoll2  44493  hoicvr  46792  hoidmv1le  46838  hoidmvle  46844  hspmbllem2  46871  smflimlem3  47017  smflimlem4  47018  smflim  47021  dfaimafn2  47412  xpiun  48404