Theorem iuneq2dv 5039

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  iuneq12dOLD  5043  iuneq12d  5044  iuneq2d  5045  fparlem3  8155  fparlem4  8156  oalim  8588  omlim  8589  oelim  8590  oelim2  8651  r1val3  9907  imasdsval  17575  acsfn  17717  tgidm  23008  cmpsub  23429  alexsublem  24073  bcth3  25384  ovoliunlem1  25556  voliunlem1  25604  uniiccdif  25632  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem4  25640  itg2monolem1  25805  taylpfval  26424  ofpreima2  32684  fnpreimac  32689  ssdifidllem  33449  esum2dlem  34056  eulerpartlemgu  34342  cvmscld  35241  satom  35324  msubvrs  35528  mblfinlem2  37618  ftc1anclem6  37658  heibor  37781  prjspval2  42568  trclfvcom  43685  scottrankd  44217  meaiininclem  46407  carageniuncllem2  46443  hoidmv1le  46515  hoidmvle  46521  ovnhoilem2  46523  ovnhoi  46524  ovnlecvr2  46531  ovncvr2  46532  hspmbl  46550  ovolval4lem1  46570  ovnovollem1  46577  ovnovollem2  46578  iunhoiioo  46597  vonioolem2  46602  smflimlem4  46695  smflimlem6  46697