Theorem iuneq1d 4978

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3897  df-iun 4952

This theorem is used by:  disjxiun  5099  kmlem11  10246  indval2  12332  prmreclem4  17106  imasval  17692  iundisj  25878  iundisj2  25879  voliunlem1  25880  iunmbl  25883  volsup  25886  uniioombllem4  25916  iuninc  33206  iundisjf  33234  iundisj2f  33235  suppovss  33325  iundisjfi  33438  iundisj2fi  33439  iundisjcnt  33440  sigaclcu3  34804  fiunelros  34857  meascnbl  34902  bnj1113  35466  bnj155  35559  bnj570  35585  bnj893  35608  cvmliftlem10  36149  mrsubvrs  36377  msubvrs  36415  voliunnfl  38691  volsupnfl  38692  heiborlem3  38856  heibor  38864  iunrelexp0  44811  iunp1  46191  iundjiunlem  47577  iundjiun  47578  meaiuninclem  47598  meaiuninc  47599  carageniuncllem1  47639  carageniuncllem2  47640  carageniuncl  47641  caratheodorylem1  47644  caratheodorylem2  47645  imasubclem3  50330  imaf1hom  50332