Theorem iuneq1d 4986

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  iuneq12dOLD  4987  disjxiun  5107  kmlem11  10121  prmreclem4  16897  imasval  17481  iundisj  25456  iundisj2  25457  voliunlem1  25458  iunmbl  25461  volsup  25464  uniioombllem4  25494  iuninc  32496  iundisjf  32525  iundisj2f  32526  suppovss  32611  iundisjfi  32726  iundisj2fi  32727  iundisjcnt  32728  indval2  32784  sigaclcu3  34119  fiunelros  34171  meascnbl  34216  bnj1113  34782  bnj155  34876  bnj570  34902  bnj893  34925  cvmliftlem10  35288  mrsubvrs  35516  msubvrs  35554  voliunnfl  37665  volsupnfl  37666  heiborlem3  37814  heibor  37822  iunrelexp0  43698  iunp1  45067  iundjiunlem  46464  iundjiun  46465  meaiuninclem  46485  meaiuninc  46486  carageniuncllem1  46526  carageniuncllem2  46527  carageniuncl  46528  caratheodorylem1  46531  caratheodorylem2  46532  imasubclem3  49099  imaf1hom  49101