Theorem iuneq12d 4952

Description: Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)

Hypotheses

Ref	Expression
iuneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
iuneq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
iuneq12d	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem iuneq12d

Step	Hyp	Ref	Expression
1		iuneq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	iuneq1d 4951	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
3		iuneq12d.2	. . . 4 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)
5	4	iuneq2dv 4948	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
6	2, 5	eqtrd 2778	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-iun 4926

This theorem is referenced by:  disjiunb  5063  cfsmolem  10026  cfsmo  10027  wunex2  10494  wuncval2  10503  imasval  17222  lpival  20516  cnextval  23212  cnextfval  23213  dvfval  25061  fedgmullem1  31710  mblfinlem2  35815  heiborlem10  35978  iunrelexpmin1  41316  iunrelexpmin2  41320  colleq12d  41871