Theorem iuneq1d 5023

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

Syntax hints:   → wi 4   = wceq 1539  ∪ ciun 4996

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-v 3474  df-in 3954  df-ss 3964  df-iun 4998

This theorem is referenced by:  iuneq12d  5024  disjxiun  5144  kmlem11  10157  prmreclem4  16856  imasval  17461  iundisj  25297  iundisj2  25298  voliunlem1  25299  iunmbl  25302  volsup  25305  uniioombllem4  25335  iuninc  32059  iundisjf  32087  iundisj2f  32088  suppovss  32173  iundisjfi  32274  iundisj2fi  32275  iundisjcnt  32276  indval2  33310  sigaclcu3  33418  fiunelros  33470  meascnbl  33515  bnj1113  34094  bnj155  34188  bnj570  34214  bnj893  34237  cvmliftlem10  34583  mrsubvrs  34811  msubvrs  34849  voliunnfl  36835  volsupnfl  36836  heiborlem3  36984  heibor  36992  iunrelexp0  42755  iunp1  44054  iundjiunlem  45473  iundjiun  45474  meaiuninclem  45494  meaiuninc  45495  carageniuncllem1  45535  carageniuncllem2  45536  carageniuncl  45537  caratheodorylem1  45540  caratheodorylem2  45541