Theorem iuneq1d 4971

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

Syntax hints:   → wi 4   = wceq 1541  ∪ ciun 4943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-v 3439  df-ss 3915  df-iun 4945

This theorem is referenced by:  iuneq12dOLD  4972  disjxiun  5092  kmlem11  10063  prmreclem4  16838  imasval  17423  iundisj  25496  iundisj2  25497  voliunlem1  25498  iunmbl  25501  volsup  25504  uniioombllem4  25534  iuninc  32561  iundisjf  32590  iundisj2f  32591  suppovss  32686  iundisjfi  32804  iundisj2fi  32805  iundisjcnt  32806  indval2  32861  sigaclcu3  34207  fiunelros  34259  meascnbl  34304  bnj1113  34869  bnj155  34963  bnj570  34989  bnj893  35012  cvmliftlem10  35410  mrsubvrs  35638  msubvrs  35676  voliunnfl  37777  volsupnfl  37778  heiborlem3  37926  heibor  37934  iunrelexp0  43859  iunp1  45227  iundjiunlem  46619  iundjiun  46620  meaiuninclem  46640  meaiuninc  46641  carageniuncllem1  46681  carageniuncllem2  46682  carageniuncl  46683  caratheodorylem1  46686  caratheodorylem2  46687  imasubclem3  49267  imaf1hom  49269