Theorem iuneq1d 4931

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

Syntax hints:   → wi 4   = wceq 1543  ∪ ciun 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883  df-iun 4906

This theorem is referenced by:  iuneq12d  4932  disjxiun  5050  kmlem11  9774  prmreclem4  16472  imasval  17016  iundisj  24445  iundisj2  24446  voliunlem1  24447  iunmbl  24450  volsup  24453  uniioombllem4  24483  iuninc  30619  iundisjf  30647  iundisj2f  30648  suppovss  30737  iundisjfi  30837  iundisj2fi  30838  iundisjcnt  30839  indval2  31694  sigaclcu3  31802  fiunelros  31854  meascnbl  31899  bnj1113  32478  bnj155  32572  bnj570  32598  bnj893  32621  cvmliftlem10  32969  mrsubvrs  33197  msubvrs  33235  voliunnfl  35558  volsupnfl  35559  heiborlem3  35708  heibor  35716  iunrelexp0  40987  iunp1  42287  iundjiunlem  43672  iundjiun  43673  meaiuninclem  43693  meaiuninc  43694  carageniuncllem1  43734  carageniuncllem2  43735  carageniuncl  43736  caratheodorylem1  43739  caratheodorylem2  43740