Theorem iuneq2dv 4478

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 2949	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4473	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457

This theorem is referenced by:  iuneq12d  4482  iuneq2d  4483  fparlem3  7166  fparlem4  7167  oalim  7499  omlim  7500  oelim  7501  oelim2  7562  r1val3  8584  imasdsval  15998  acsfn  16143  tgidm  20595  cmpsub  21013  alexsublem  21658  bcth3  22936  ovoliunlem1  23077  voliunlem1  23125  uniiccdif  23152  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem4  23160  itg2monolem1  23323  taylpfval  23923  ofpreima2  28849  esum2dlem  29481  eulerpartlemgu  29766  cvmscld  30509  msubvrs  30711  mblfinlem2  32617  ftc1anclem6  32660  heibor  32790  trclfvcom  37034  meaiininclem  39376  carageniuncllem2  39412  hoidmv1le  39484  hoidmvle  39490  ovnhoilem2  39492  ovnhoi  39493  ovnlecvr2  39500  ovncvr2  39501  hspmbl  39519  ovolval4lem1  39539  ovnovollem1  39546  ovnovollem2  39547  iunhoiioo  39567  vonioolem2  39572  smflimlem4  39660  smflimlem6  39662