Theorem iuneq2dv 4686

Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)

Hypothesis

Ref	Expression
iuneq2dv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2dv	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2dv

Step	Hyp	Ref	Expression
1		iuneq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3096	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4681	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624   ∈ wcel 2131  ∀wral 3042  ∪ ciun 4664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-v 3334  df-in 3714  df-ss 3721  df-iun 4666

This theorem is referenced by:  iuneq12d  4690  iuneq2d  4691  fparlem3  7439  fparlem4  7440  oalim  7773  omlim  7774  oelim  7775  oelim2  7836  r1val3  8866  imasdsval  16369  acsfn  16513  tgidm  20978  cmpsub  21397  alexsublem  22041  bcth3  23320  ovoliunlem1  23462  voliunlem1  23510  uniiccdif  23538  uniioombllem2  23543  uniioombllem3a  23544  uniioombllem4  23546  itg2monolem1  23708  taylpfval  24310  ofpreima2  29767  esum2dlem  30455  eulerpartlemgu  30740  cvmscld  31554  msubvrs  31756  mblfinlem2  33752  ftc1anclem6  33795  heibor  33925  trclfvcom  38509  meaiininclem  41198  carageniuncllem2  41234  hoidmv1le  41306  hoidmvle  41312  ovnhoilem2  41314  ovnhoi  41315  ovnlecvr2  41322  ovncvr2  41323  hspmbl  41341  ovolval4lem1  41361  ovnovollem1  41368  ovnovollem2  41369  iunhoiioo  41388  vonioolem2  41393  smflimlem4  41480  smflimlem6  41482