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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  disjxiun  5100  kmlem11  10232  indval2  12318  prmreclem4  17090  imasval  17676  iundisj  25862  iundisj2  25863  voliunlem1  25864  iunmbl  25867  volsup  25870  uniioombllem4  25900  iuninc  33148  iundisjf  33176  iundisj2f  33177  suppovss  33267  iundisjfi  33381  iundisj2fi  33382  iundisjcnt  33383  sigaclcu3  34747  fiunelros  34800  meascnbl  34845  bnj1113  35409  bnj155  35502  bnj570  35528  bnj893  35551  cvmliftlem10  36038  mrsubvrs  36266  msubvrs  36304  voliunnfl  38562  volsupnfl  38563  heiborlem3  38727  heibor  38735  iunrelexp0  44687  iunp1  46052  iundjiunlem  47438  iundjiun  47439  meaiuninclem  47459  meaiuninc  47460  carageniuncllem1  47500  carageniuncllem2  47501  carageniuncl  47502  caratheodorylem1  47505  caratheodorylem2  47506  imasubclem3  50183  imaf1hom  50185