Theorem iuneq1d 4976

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

Syntax hints:   → wi 4   = wceq 1542  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  iuneq12dOLD  4977  disjxiun  5097  kmlem11  10083  prmreclem4  16859  imasval  17444  iundisj  25517  iundisj2  25518  voliunlem1  25519  iunmbl  25522  volsup  25525  uniioombllem4  25555  iuninc  32647  iundisjf  32676  iundisj2f  32677  suppovss  32771  iundisjfi  32887  iundisj2fi  32888  iundisjcnt  32889  indval2  32944  sigaclcu3  34300  fiunelros  34352  meascnbl  34397  bnj1113  34962  bnj155  35055  bnj570  35081  bnj893  35104  cvmliftlem10  35510  mrsubvrs  35738  msubvrs  35776  voliunnfl  37915  volsupnfl  37916  heiborlem3  38064  heibor  38072  iunrelexp0  44058  iunp1  45426  iundjiunlem  46817  iundjiun  46818  meaiuninclem  46838  meaiuninc  46839  carageniuncllem1  46879  carageniuncllem2  46880  carageniuncl  46881  caratheodorylem1  46884  caratheodorylem2  46885  imasubclem3  49465  imaf1hom  49467