Theorem iuneq1d 4974

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

Syntax hints:   → wi 4   = wceq 1541  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-v 3442  df-ss 3918  df-iun 4948

This theorem is referenced by:  iuneq12dOLD  4975  disjxiun  5095  kmlem11  10071  prmreclem4  16847  imasval  17432  iundisj  25505  iundisj2  25506  voliunlem1  25507  iunmbl  25510  volsup  25513  uniioombllem4  25543  iuninc  32635  iundisjf  32664  iundisj2f  32665  suppovss  32760  iundisjfi  32876  iundisj2fi  32877  iundisjcnt  32878  indval2  32933  sigaclcu3  34279  fiunelros  34331  meascnbl  34376  bnj1113  34941  bnj155  35035  bnj570  35061  bnj893  35084  cvmliftlem10  35488  mrsubvrs  35716  msubvrs  35754  voliunnfl  37865  volsupnfl  37866  heiborlem3  38014  heibor  38022  iunrelexp0  43943  iunp1  45311  iundjiunlem  46703  iundjiun  46704  meaiuninclem  46724  meaiuninc  46725  carageniuncllem1  46765  carageniuncllem2  46766  carageniuncl  46767  caratheodorylem1  46770  caratheodorylem2  46771  imasubclem3  49351  imaf1hom  49353