Theorem iuneq1d 4481

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

Syntax hints:   → wi 4   = wceq 1475  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457

This theorem is referenced by:  iuneq12d  4482  disjxiun  4579  disjxiunOLD  4580  kmlem11  8865  prmreclem4  15461  imasval  15994  iundisj  23123  iundisj2  23124  voliunlem1  23125  iunmbl  23128  volsup  23131  uniioombllem4  23160  iuninc  28761  iundisjf  28784  iundisj2f  28785  iundisjfi  28942  iundisj2fi  28943  iundisjcnt  28944  indval2  29404  sigaclcu3  29512  fiunelros  29564  meascnbl  29609  bnj1113  30110  bnj155  30203  bnj570  30229  bnj893  30252  cvmliftlem10  30530  mrsubvrs  30673  msubvrs  30711  voliunnfl  32623  volsupnfl  32624  heiborlem3  32782  heibor  32790  iunrelexp0  37013  iunp1  38260  iundjiunlem  39352  iundjiun  39353  meaiuninclem  39373  meaiuninc  39374  carageniuncllem1  39411  carageniuncllem2  39412  carageniuncl  39413  caratheodorylem1  39416  caratheodorylem2  39417