Theorem iuneq1d 5024

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-v 3476  df-in 3955  df-ss 3965  df-iun 4999

This theorem is referenced by:  iuneq12d  5025  disjxiun  5145  kmlem11  10157  prmreclem4  16856  imasval  17461  iundisj  25289  iundisj2  25290  voliunlem1  25291  iunmbl  25294  volsup  25297  uniioombllem4  25327  iuninc  32047  iundisjf  32075  iundisj2f  32076  suppovss  32161  iundisjfi  32262  iundisj2fi  32263  iundisjcnt  32264  indval2  33298  sigaclcu3  33406  fiunelros  33458  meascnbl  33503  bnj1113  34082  bnj155  34176  bnj570  34202  bnj893  34225  cvmliftlem10  34571  mrsubvrs  34799  msubvrs  34837  voliunnfl  36835  volsupnfl  36836  heiborlem3  36984  heibor  36992  iunrelexp0  42755  iunp1  44055  iundjiunlem  45474  iundjiun  45475  meaiuninclem  45495  meaiuninc  45496  carageniuncllem1  45536  carageniuncllem2  45537  carageniuncl  45538  caratheodorylem1  45541  caratheodorylem2  45542