Theorem iuneq1d 4995

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  iuneq12dOLD  4996  disjxiun  5116  kmlem11  10175  prmreclem4  16939  imasval  17525  iundisj  25501  iundisj2  25502  voliunlem1  25503  iunmbl  25506  volsup  25509  uniioombllem4  25539  iuninc  32541  iundisjf  32570  iundisj2f  32571  suppovss  32658  iundisjfi  32773  iundisj2fi  32774  iundisjcnt  32775  indval2  32831  sigaclcu3  34153  fiunelros  34205  meascnbl  34250  bnj1113  34816  bnj155  34910  bnj570  34936  bnj893  34959  cvmliftlem10  35316  mrsubvrs  35544  msubvrs  35582  voliunnfl  37688  volsupnfl  37689  heiborlem3  37837  heibor  37845  iunrelexp0  43726  iunp1  45090  iundjiunlem  46488  iundjiun  46489  meaiuninclem  46509  meaiuninc  46510  carageniuncllem1  46550  carageniuncllem2  46551  carageniuncl  46552  caratheodorylem1  46555  caratheodorylem2  46556  imasubclem3  49065  imaf1hom  49067