Theorem iuneq2i 4902

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∪ ciun 4881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-iun 4883

This theorem is referenced by:  dfiunv2  4922  iunrab  4939  iunid  4947  iunin1  4957  2iunin  4961  resiun1  5838  resiun2  5839  dfimafn2  6704  dfmpt  6883  funiunfv  6985  fpar  7794  onovuni  7962  uniqs  8340  marypha2lem2  8884  alephlim  9478  cfsmolem  9681  ituniiun  9833  imasdsval2  16781  lpival  20011  cmpsublem  22004  txbasval  22211  uniioombllem2  24187  uniioombllem4  24190  volsup2  24209  itg1addlem5  24304  itg1climres  24318  indval2  31383  sigaclfu2  31490  measvuni  31583  fmla  32741  trpred0  33188  rabiun  35030  mblfinlem2  35095  voliunnfl  35101  cnambfre  35105  uniqsALTV  35746  trclrelexplem  40412  cotrclrcl  40443  dfcoll2  40960  hoicvr  43187  hoidmv1le  43233  hoidmvle  43239  hspmbllem2  43266  smflimlem3  43406  smflimlem4  43407  smflim  43410  dfaimafn2  43722  xpiun  44386