Theorem iuneq1d 4972

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3440  df-ss 3922  df-iun 4946

This theorem is referenced by:  iuneq12dOLD  4973  disjxiun  5092  kmlem11  10074  prmreclem4  16850  imasval  17434  iundisj  25466  iundisj2  25467  voliunlem1  25468  iunmbl  25471  volsup  25474  uniioombllem4  25504  iuninc  32523  iundisjf  32552  iundisj2f  32553  suppovss  32642  iundisjfi  32758  iundisj2fi  32759  iundisjcnt  32760  indval2  32816  sigaclcu3  34108  fiunelros  34160  meascnbl  34205  bnj1113  34771  bnj155  34865  bnj570  34891  bnj893  34914  cvmliftlem10  35286  mrsubvrs  35514  msubvrs  35552  voliunnfl  37663  volsupnfl  37664  heiborlem3  37812  heibor  37820  iunrelexp0  43695  iunp1  45064  iundjiunlem  46460  iundjiun  46461  meaiuninclem  46481  meaiuninc  46482  carageniuncllem1  46522  carageniuncllem2  46523  carageniuncl  46524  caratheodorylem1  46527  caratheodorylem2  46528  imasubclem3  49111  imaf1hom  49113