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 3083	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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  dfiunv2  4992  iunrab  5011  iunin1  5030  2iunin  5036  resiun1  5990  resiun2  5991  dfimafn2  6948  dfmpt  7147  funiunfv  7252  fpar  8127  onovuni  8350  uniqs  8794  marypha2lem2  9428  alephlim  10146  cfsmolem  10348  ituniiun  10500  indval2  12325  imasdsval2  17688  lpival  21648  pzriprnglem10  21796  pzriprnglem11  21797  cmpsublem  23717  txbasval  23925  uniioombllem2  25904  uniioombllem4  25907  volsup2  25926  itg1addlem5  26021  itg1climres  26035  sigaclfu2  34753  measvuni  34847  fmla  36146  ttciun  37302  rabiun  38521  mblfinlem2  38576  voliunnfl  38582  cnambfre  38586  trclrelexplem  44710  cotrclrcl  44741  dfcoll2  45235  hoicvr  47557  hoidmv1le  47603  hoidmvle  47609  hspmbllem2  47636  smflimlem3  47782  smflimlem4  47783  smflim  47786  dfaimafn2  48235  xpiun  49255