Theorem iuneq1d 4979

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

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

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 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  iuneq12dOLD  4980  disjxiun  5099  kmlem11  10090  prmreclem4  16866  imasval  17450  iundisj  25425  iundisj2  25426  voliunlem1  25427  iunmbl  25430  volsup  25433  uniioombllem4  25463  iuninc  32462  iundisjf  32491  iundisj2f  32492  suppovss  32577  iundisjfi  32692  iundisj2fi  32693  iundisjcnt  32694  indval2  32750  sigaclcu3  34085  fiunelros  34137  meascnbl  34182  bnj1113  34748  bnj155  34842  bnj570  34868  bnj893  34891  cvmliftlem10  35254  mrsubvrs  35482  msubvrs  35520  voliunnfl  37631  volsupnfl  37632  heiborlem3  37780  heibor  37788  iunrelexp0  43664  iunp1  45033  iundjiunlem  46430  iundjiun  46431  meaiuninclem  46451  meaiuninc  46452  carageniuncllem1  46492  carageniuncllem2  46493  carageniuncl  46494  caratheodorylem1  46497  caratheodorylem2  46498  imasubclem3  49068  imaf1hom  49070