Theorem iuneq1d 4983

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

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

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 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  iuneq12dOLD  4984  disjxiun  5104  kmlem11  10114  prmreclem4  16890  imasval  17474  iundisj  25449  iundisj2  25450  voliunlem1  25451  iunmbl  25454  volsup  25457  uniioombllem4  25487  iuninc  32489  iundisjf  32518  iundisj2f  32519  suppovss  32604  iundisjfi  32719  iundisj2fi  32720  iundisjcnt  32721  indval2  32777  sigaclcu3  34112  fiunelros  34164  meascnbl  34209  bnj1113  34775  bnj155  34869  bnj570  34895  bnj893  34918  cvmliftlem10  35281  mrsubvrs  35509  msubvrs  35547  voliunnfl  37658  volsupnfl  37659  heiborlem3  37807  heibor  37815  iunrelexp0  43691  iunp1  45060  iundjiunlem  46457  iundjiun  46458  meaiuninclem  46478  meaiuninc  46479  carageniuncllem1  46519  carageniuncllem2  46520  carageniuncl  46521  caratheodorylem1  46524  caratheodorylem2  46525  imasubclem3  49095  imaf1hom  49097