Theorem iuneq2dv 4935

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ∪ ciun 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-in 3942  df-ss 3951  df-iun 4913

This theorem is referenced by:  iuneq12d  4939  iuneq2d  4940  fparlem3  7803  fparlem4  7804  oalim  8151  omlim  8152  oelim  8153  oelim2  8215  r1val3  9261  imasdsval  16782  acsfn  16924  tgidm  21582  cmpsub  22002  alexsublem  22646  bcth3  23928  ovoliunlem1  24097  voliunlem1  24145  uniiccdif  24173  uniioombllem2  24178  uniioombllem3a  24179  uniioombllem4  24181  itg2monolem1  24345  taylpfval  24947  ofpreima2  30405  fnpreimac  30410  esum2dlem  31346  eulerpartlemgu  31630  cvmscld  32515  satom  32598  msubvrs  32802  mblfinlem2  34924  ftc1anclem6  34966  heibor  35093  prjspval2  39256  trclfvcom  40061  scottrankd  40577  meaiininclem  42762  carageniuncllem2  42798  hoidmv1le  42870  hoidmvle  42876  ovnhoilem2  42878  ovnhoi  42879  ovnlecvr2  42886  ovncvr2  42887  hspmbl  42905  ovolval4lem1  42925  ovnovollem1  42932  ovnovollem2  42933  iunhoiioo  42952  vonioolem2  42957  smflimlem4  43044  smflimlem6  43046