Theorem iuneq12d 4976

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 2847	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	anbi1d 640	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑡 ∈ 𝐶)))
4	3	rexbidv2 3181	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶))
5	4	abbidv 2827	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶} = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶})
6		df-iun 4948	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶}
7		df-iun 4948	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶}
8	5, 6, 7	3eqtr4g 2821	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
9		iuneq12d.2	. . . 4 ⊢ (𝜑 → 𝐶 = 𝐷)
10	9	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)
11	10	iuneq2dv 4971	. 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
12	8, 11	eqtrd 2796	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  {cab 2739  ∃wrex 3085  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-v 3455  df-ss 3919  df-iun 4948

This theorem is referenced by:  disjiunb  5087  cfsmolem  10221  cfsmo  10222  wunex2  10690  wuncval2  10699  imasval  17532  lpival  21382  cnextval  24109  cnextfval  24110  dvfval  25947  fedgmullem1  33887  irngval  33943  mblfinlem2  38118  heiborlem10  38280  iunrelexpmin1  44245  iunrelexpmin2  44249  colleq12d  44790