Theorem iuneq1d 4986

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-v 3448  df-in 3920  df-ss 3930  df-iun 4961

This theorem is referenced by:  iuneq12d  4987  disjxiun  5107  kmlem11  10105  prmreclem4  16802  imasval  17407  iundisj  24949  iundisj2  24950  voliunlem1  24951  iunmbl  24954  volsup  24957  uniioombllem4  24987  iuninc  31546  iundisjf  31574  iundisj2f  31575  suppovss  31665  iundisjfi  31767  iundisj2fi  31768  iundisjcnt  31769  indval2  32702  sigaclcu3  32810  fiunelros  32862  meascnbl  32907  bnj1113  33486  bnj155  33580  bnj570  33606  bnj893  33629  cvmliftlem10  33975  mrsubvrs  34203  msubvrs  34241  voliunnfl  36195  volsupnfl  36196  heiborlem3  36345  heibor  36353  iunrelexp0  42096  iunp1  43396  iundjiunlem  44820  iundjiun  44821  meaiuninclem  44841  meaiuninc  44842  carageniuncllem1  44882  carageniuncllem2  44883  carageniuncl  44884  caratheodorylem1  44887  caratheodorylem2  44888