Theorem iuneq2i 4978

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is referenced by:  dfiunv2  4998  iunrab  5017  iunin1  5036  2iunin  5042  resiun1  5998  resiun2  5999  dfimafn2  6944  dfmpt  7140  funiunfv  7246  fpar  8107  onovuni  8325  uniqs  8767  marypha2lem2  9392  alephlim  10047  cfsmolem  10249  ituniiun  10401  indval2  12218  imasdsval2  17565  lpival  21492  pzriprnglem10  21640  pzriprnglem11  21641  cmpsublem  23556  txbasval  23763  uniioombllem2  25742  uniioombllem4  25745  volsup2  25764  itg1addlem5  25859  itg1climres  25873  sigaclfu2  34511  measvuni  34604  fmla  35873  ttciun  37025  rabiun  38244  mblfinlem2  38309  voliunnfl  38315  cnambfre  38319  trclrelexplem  44437  cotrclrcl  44468  dfcoll2  44962  hoicvr  47262  hoidmv1le  47308  hoidmvle  47314  hspmbllem2  47341  smflimlem3  47487  smflimlem4  47488  smflim  47491  dfaimafn2  47903  xpiun  48923