Theorem iuneq1d 5019

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

Syntax hints:   → wi 4   = wceq 1540  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  iuneq12dOLD  5020  disjxiun  5140  kmlem11  10201  prmreclem4  16957  imasval  17556  iundisj  25583  iundisj2  25584  voliunlem1  25585  iunmbl  25588  volsup  25591  uniioombllem4  25621  iuninc  32573  iundisjf  32602  iundisj2f  32603  suppovss  32690  iundisjfi  32798  iundisj2fi  32799  iundisjcnt  32800  indval2  32839  sigaclcu3  34123  fiunelros  34175  meascnbl  34220  bnj1113  34799  bnj155  34893  bnj570  34919  bnj893  34942  cvmliftlem10  35299  mrsubvrs  35527  msubvrs  35565  voliunnfl  37671  volsupnfl  37672  heiborlem3  37820  heibor  37828  iunrelexp0  43715  iunp1  45071  iundjiunlem  46474  iundjiun  46475  meaiuninclem  46495  meaiuninc  46496  carageniuncllem1  46536  carageniuncllem2  46537  carageniuncl  46538  caratheodorylem1  46541  caratheodorylem2  46542