Theorem iuneq2i 4955

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  dfiunv2  4976  iunrab  4995  iunin1  5014  2iunin  5018  resiun1  5964  resiun2  5965  dfimafn2  6903  dfmpt  7097  funiunfv  7203  fpar  8066  onovuni  8282  uniqs  8720  marypha2lem2  9349  alephlim  9989  cfsmolem  10192  ituniiun  10344  indval2  12164  imasdsval2  17480  lpival  21322  pzriprnglem10  21470  pzriprnglem11  21471  cmpsublem  23364  txbasval  23571  uniioombllem2  25550  uniioombllem4  25553  volsup2  25572  itg1addlem5  25667  itg1climres  25681  sigaclfu2  34265  measvuni  34358  fmla  35563  ttciun  36696  rabiun  37914  mblfinlem2  37979  voliunnfl  37985  cnambfre  37989  trclrelexplem  44138  cotrclrcl  44169  dfcoll2  44679  hoicvr  46976  hoidmv1le  47022  hoidmvle  47028  hspmbllem2  47055  smflimlem3  47201  smflimlem4  47202  smflim  47205  dfaimafn2  47614  xpiun  48634