Theorem iuneq1d 5042

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

Syntax hints:   → wi 4   = wceq 1537  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  iuneq12dOLD  5043  disjxiun  5163  kmlem11  10230  prmreclem4  16966  imasval  17571  iundisj  25602  iundisj2  25603  voliunlem1  25604  iunmbl  25607  volsup  25610  uniioombllem4  25640  iuninc  32583  iundisjf  32611  iundisj2f  32612  suppovss  32697  iundisjfi  32801  iundisj2fi  32802  iundisjcnt  32803  indval2  33978  sigaclcu3  34086  fiunelros  34138  meascnbl  34183  bnj1113  34761  bnj155  34855  bnj570  34881  bnj893  34904  cvmliftlem10  35262  mrsubvrs  35490  msubvrs  35528  voliunnfl  37624  volsupnfl  37625  heiborlem3  37773  heibor  37781  iunrelexp0  43664  iunp1  44968  iundjiunlem  46380  iundjiun  46381  meaiuninclem  46401  meaiuninc  46402  carageniuncllem1  46442  carageniuncllem2  46443  carageniuncl  46444  caratheodorylem1  46447  caratheodorylem2  46448