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 18	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  iuneq12dOLD  4987  disjxiun  5108  kmlem11  10160  indval2  12238  prmreclem4  17001  imasval  17587  iundisj  25758  iundisj2  25759  voliunlem1  25760  iunmbl  25763  volsup  25766  uniioombllem4  25796  iuninc  32976  iundisjf  33005  iundisj2f  33006  suppovss  33097  iundisjfi  33211  iundisj2fi  33212  iundisjcnt  33213  sigaclcu3  34576  fiunelros  34629  meascnbl  34674  bnj1113  35239  bnj155  35332  bnj570  35358  bnj893  35381  cvmliftlem10  35823  mrsubvrs  36051  msubvrs  36089  voliunnfl  38372  volsupnfl  38373  heiborlem3  38522  heibor  38530  iunrelexp0  44486  iunp1  45844  iundjiunlem  47231  iundjiun  47232  meaiuninclem  47252  meaiuninc  47253  carageniuncllem1  47293  carageniuncllem2  47294  carageniuncl  47295  caratheodorylem1  47298  caratheodorylem2  47299  imasubclem3  49941  imaf1hom  49943