Theorem iuneq1d 5024

Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)

Hypothesis

Ref	Expression
iuneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq1d

Step	Hyp	Ref	Expression
1		iuneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		iuneq1 5013	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   = wceq 1537  ∪ ciun 4996

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-v 3480  df-ss 3980  df-iun 4998

This theorem is referenced by:  iuneq12dOLD  5025  disjxiun  5145  kmlem11  10199  prmreclem4  16953  imasval  17558  iundisj  25597  iundisj2  25598  voliunlem1  25599  iunmbl  25602  volsup  25605  uniioombllem4  25635  iuninc  32581  iundisjf  32609  iundisj2f  32610  suppovss  32696  iundisjfi  32804  iundisj2fi  32805  iundisjcnt  32806  indval2  33995  sigaclcu3  34103  fiunelros  34155  meascnbl  34200  bnj1113  34778  bnj155  34872  bnj570  34898  bnj893  34921  cvmliftlem10  35279  mrsubvrs  35507  msubvrs  35545  voliunnfl  37651  volsupnfl  37652  heiborlem3  37800  heibor  37808  iunrelexp0  43692  iunp1  45006  iundjiunlem  46415  iundjiun  46416  meaiuninclem  46436  meaiuninc  46437  carageniuncllem1  46477  carageniuncllem2  46478  carageniuncl  46479  caratheodorylem1  46482  caratheodorylem2  46483