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 3050	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ ciun 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  dfiunv2  4994  iunrab  5011  iunidOLD  5020  iunin1  5031  2iunin  5035  resiun1  5959  resiun2  5960  dfimafn2  6906  dfmpt  7098  funiunfv  7204  fpar  8072  onovuni  8288  uniqs  8724  marypha2lem2  9363  alephlim  9996  cfsmolem  10199  ituniiun  10351  imasdsval2  17455  lpival  21210  pzriprnglem10  21376  pzriprnglem11  21377  cmpsublem  23262  txbasval  23469  uniioombllem2  25460  uniioombllem4  25463  volsup2  25482  itg1addlem5  25577  itg1climres  25591  indval2  32750  sigaclfu2  34084  measvuni  34177  fmla  35341  rabiun  37560  mblfinlem2  37625  voliunnfl  37631  cnambfre  37635  trclrelexplem  43673  cotrclrcl  43704  dfcoll2  44214  hoicvr  46519  hoidmv1le  46565  hoidmvle  46571  hspmbllem2  46598  smflimlem3  46744  smflimlem4  46745  smflim  46748  dfaimafn2  47140  xpiun  48119