Theorem iuneq12d 5002

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 2821	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	anbi1d 631	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑡 ∈ 𝐶)))
4	3	rexbidv2 3161	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶))
5	4	abbidv 2802	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶} = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶})
6		df-iun 4974	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶}
7		df-iun 4974	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶}
8	5, 6, 7	3eqtr4g 2796	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
9		iuneq12d.2	. . . 4 ⊢ (𝜑 → 𝐶 = 𝐷)
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)
11	10	iuneq2dv 4997	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
12	8, 11	eqtrd 2771	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2714  ∃wrex 3061  ∪ ciun 4972

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-v 3466  df-ss 3948  df-iun 4974

This theorem is referenced by:  disjiunb  5114  cfsmolem  10289  cfsmo  10290  wunex2  10757  wuncval2  10766  imasval  17530  lpival  21290  cnextval  24004  cnextfval  24005  dvfval  25855  fedgmullem1  33674  irngval  33731  mblfinlem2  37687  heiborlem10  37849  iunrelexpmin1  43699  iunrelexpmin2  43703  colleq12d  44244