Metamath Proof Explorer


Theorem iuneq12d

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

Ref Expression
Hypotheses iuneq12d.1 φ A = B
iuneq12d.2 φ C = D
Assertion iuneq12d φ x A C = x B D

Proof

Step Hyp Ref Expression
1 iuneq12d.1 φ A = B
2 iuneq12d.2 φ C = D
3 1 eleq2d φ x A x B
4 3 anbi1d φ x A t C x B t C
5 4 rexbidv2 φ x A t C x B t C
6 5 abbidv φ t | x A t C = t | x B t C
7 df-iun x A C = t | x A t C
8 df-iun x B C = t | x B t C
9 6 7 8 3eqtr4g φ x A C = x B C
10 2 adantr φ x B C = D
11 10 iuneq2dv φ x B C = x B D
12 9 11 eqtrd φ x A C = x B D