Theorem iuneq1d 4961

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

Syntax hints:   → wi 4   = wceq 1542  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  iuneq12dOLD  4962  disjxiun  5082  kmlem11  10083  indval2  12164  prmreclem4  16890  imasval  17475  iundisj  25515  iundisj2  25516  voliunlem1  25517  iunmbl  25520  volsup  25523  uniioombllem4  25553  iuninc  32630  iundisjf  32659  iundisj2f  32660  suppovss  32754  iundisjfi  32869  iundisj2fi  32870  iundisjcnt  32871  sigaclcu3  34266  fiunelros  34318  meascnbl  34363  bnj1113  34928  bnj155  35021  bnj570  35047  bnj893  35070  cvmliftlem10  35476  mrsubvrs  35704  msubvrs  35742  voliunnfl  37985  volsupnfl  37986  heiborlem3  38134  heibor  38142  iunrelexp0  44129  iunp1  45497  iundjiunlem  46887  iundjiun  46888  meaiuninclem  46908  meaiuninc  46909  carageniuncllem1  46949  carageniuncllem2  46950  carageniuncl  46951  caratheodorylem1  46954  caratheodorylem2  46955  imasubclem3  49581  imaf1hom  49583