Theorem iuneq12d 5026

Description: Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) Remove DV conditions (Revised by GG, 1-Sep-2025.)

Hypotheses

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

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem iuneq12d

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iuneq12d.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eleq2d 2825	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	anbi1d 631	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑡 ∈ 𝐶)))
4	3	rexbidv2 3173	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶))
5	4	abbidv 2806	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶} = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶})
6		df-iun 4998	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶}
7		df-iun 4998	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶}
8	5, 6, 7	3eqtr4g 2800	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
9		iuneq12d.2	. . . 4 ⊢ (𝜑 → 𝐶 = 𝐷)
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)
11	10	iuneq2dv 5021	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
12	8, 11	eqtrd 2775	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  {cab 2712  ∃wrex 3068  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-iun 4998

This theorem is referenced by:  disjiunb  5138  cfsmolem  10308  cfsmo  10309  wunex2  10776  wuncval2  10785  imasval  17558  lpival  21352  cnextval  24085  cnextfval  24086  dvfval  25947  fedgmullem1  33657  irngval  33700  mblfinlem2  37645  heiborlem10  37807  iunrelexpmin1  43698  iunrelexpmin2  43702  colleq12d  44249