Theorem iuneq1d 4979

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  disjxiun  5100  kmlem11  10163  indval2  12247  prmreclem4  17011  imasval  17597  iundisj  25776  iundisj2  25777  voliunlem1  25778  iunmbl  25781  volsup  25784  uniioombllem4  25814  iuninc  33034  iundisjf  33062  iundisj2f  33063  suppovss  33153  iundisjfi  33267  iundisj2fi  33268  iundisjcnt  33269  sigaclcu3  34632  fiunelros  34685  meascnbl  34730  bnj1113  35295  bnj155  35388  bnj570  35414  bnj893  35437  cvmliftlem10  35873  mrsubvrs  36101  msubvrs  36139  voliunnfl  38413  volsupnfl  38414  heiborlem3  38563  heibor  38571  iunrelexp0  44542  iunp1  45900  iundjiunlem  47287  iundjiun  47288  meaiuninclem  47308  meaiuninc  47309  carageniuncllem1  47349  carageniuncllem2  47350  carageniuncl  47351  caratheodorylem1  47354  caratheodorylem2  47355  imasubclem3  50032  imaf1hom  50034