Theorem iuneq2i 4945

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-iun 4926

This theorem is referenced by:  dfiunv2  4965  iunrab  4982  iunid  4990  iunin1  5001  2iunin  5005  resiun1  5911  resiun2  5912  dfimafn2  6833  dfmpt  7016  funiunfv  7121  fpar  7956  onovuni  8173  uniqs  8566  marypha2lem2  9195  alephlim  9823  cfsmolem  10026  ituniiun  10178  imasdsval2  17227  lpival  20516  cmpsublem  22550  txbasval  22757  uniioombllem2  24747  uniioombllem4  24750  volsup2  24769  itg1addlem5  24865  itg1climres  24879  indval2  31982  sigaclfu2  32089  measvuni  32182  fmla  33343  rabiun  35750  mblfinlem2  35815  voliunnfl  35821  cnambfre  35825  uniqsALTV  36464  trclrelexplem  41319  cotrclrcl  41350  dfcoll2  41870  hoicvr  44086  hoidmv1le  44132  hoidmvle  44138  hspmbllem2  44165  smflimlem3  44308  smflimlem4  44309  smflim  44312  dfaimafn2  44658  xpiun  45320