Theorem iuneq1d 4948

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

Syntax hints:   → wi 4   = wceq 1539  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-in 3890  df-ss 3900  df-iun 4923

This theorem is referenced by:  iuneq12d  4949  disjxiun  5067  kmlem11  9847  prmreclem4  16548  imasval  17139  iundisj  24617  iundisj2  24618  voliunlem1  24619  iunmbl  24622  volsup  24625  uniioombllem4  24655  iuninc  30801  iundisjf  30829  iundisj2f  30830  suppovss  30919  iundisjfi  31019  iundisj2fi  31020  iundisjcnt  31021  indval2  31882  sigaclcu3  31990  fiunelros  32042  meascnbl  32087  bnj1113  32665  bnj155  32759  bnj570  32785  bnj893  32808  cvmliftlem10  33156  mrsubvrs  33384  msubvrs  33422  voliunnfl  35748  volsupnfl  35749  heiborlem3  35898  heibor  35906  iunrelexp0  41199  iunp1  42503  iundjiunlem  43887  iundjiun  43888  meaiuninclem  43908  meaiuninc  43909  carageniuncllem1  43949  carageniuncllem2  43950  carageniuncl  43951  caratheodorylem1  43954  caratheodorylem2  43955