Theorem iuneq1d 4984

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4958

This theorem is used by:  disjxiun  5105  kmlem11  10278  indval2  12365  prmreclem4  17141  imasval  17733  iundisj  25924  iundisj2  25925  voliunlem1  25926  iunmbl  25929  volsup  25932  uniioombllem4  25962  iuninc  33253  iundisjf  33281  iundisj2f  33282  suppovss  33371  iundisjfi  33484  iundisj2fi  33485  iundisjcnt  33486  sigaclcu3  34865  fiunelros  34918  meascnbl  34963  bnj1113  35527  bnj155  35620  bnj570  35646  bnj893  35669  cvmliftlem10  36267  mrsubvrs  36495  msubvrs  36533  voliunnfl  38850  volsupnfl  38851  heiborlem3  39013  heibor  39021  iunrelexp0  44963  iunp1  46357  iundjiunlem  47742  iundjiun  47743  meaiuninclem  47763  meaiuninc  47764  carageniuncllem1  47804  carageniuncllem2  47805  carageniuncl  47806  caratheodorylem1  47809  caratheodorylem2  47810  imasubclem3  50553  imaf1hom  50555