Theorem iuneq12d 4985

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 2814	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	anbi1d 631	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑡 ∈ 𝐶)))
4	3	rexbidv2 3153	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶))
5	4	abbidv 2795	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶} = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶})
6		df-iun 4957	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶}
7		df-iun 4957	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶}
8	5, 6, 7	3eqtr4g 2789	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
9		iuneq12d.2	. . . 4 ⊢ (𝜑 → 𝐶 = 𝐷)
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)
11	10	iuneq2dv 4980	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
12	8, 11	eqtrd 2764	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  disjiunb  5097  cfsmolem  10223  cfsmo  10224  wunex2  10691  wuncval2  10700  imasval  17474  lpival  21234  cnextval  23948  cnextfval  23949  dvfval  25798  fedgmullem1  33625  irngval  33680  mblfinlem2  37652  heiborlem10  37814  iunrelexpmin1  43697  iunrelexpmin2  43701  colleq12d  44242