Theorem iuneq1d 4984

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

Syntax hints:   → wi 4   = wceq 1570  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is referenced by:  iuneq12dOLD  4985  disjxiun  5106  kmlem11  10140  indval2  12218  prmreclem4  16974  imasval  17560  iundisj  25707  iundisj2  25708  voliunlem1  25709  iunmbl  25712  volsup  25715  uniioombllem4  25745  iuninc  32905  iundisjf  32934  iundisj2f  32935  suppovss  33026  iundisjfi  33141  iundisj2fi  33142  iundisjcnt  33143  sigaclcu3  34512  fiunelros  34564  meascnbl  34609  bnj1113  35174  bnj155  35267  bnj570  35293  bnj893  35316  cvmliftlem10  35786  mrsubvrs  36014  msubvrs  36052  voliunnfl  38315  volsupnfl  38316  heiborlem3  38464  heibor  38472  iunrelexp0  44428  iunp1  45786  iundjiunlem  47173  iundjiun  47174  meaiuninclem  47194  meaiuninc  47195  carageniuncllem1  47235  carageniuncllem2  47236  carageniuncl  47237  caratheodorylem1  47240  caratheodorylem2  47241  imasubclem3  49884  imaf1hom  49886