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 ( 𝜑𝐴 = 𝐵 )
iuneq12d.2 ( 𝜑𝐶 = 𝐷 )
Assertion iuneq12d ( 𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 iuneq12d.1 ( 𝜑𝐴 = 𝐵 )
2 iuneq12d.2 ( 𝜑𝐶 = 𝐷 )
3 1 eleq2d ( 𝜑 → ( 𝑥𝐴𝑥𝐵 ) )
4 3 anbi1d ( 𝜑 → ( ( 𝑥𝐴𝑡𝐶 ) ↔ ( 𝑥𝐵𝑡𝐶 ) ) )
5 4 rexbidv2 ( 𝜑 → ( ∃ 𝑥𝐴 𝑡𝐶 ↔ ∃ 𝑥𝐵 𝑡𝐶 ) )
6 5 abbidv ( 𝜑 → { 𝑡 ∣ ∃ 𝑥𝐴 𝑡𝐶 } = { 𝑡 ∣ ∃ 𝑥𝐵 𝑡𝐶 } )
7 df-iun 𝑥𝐴 𝐶 = { 𝑡 ∣ ∃ 𝑥𝐴 𝑡𝐶 }
8 df-iun 𝑥𝐵 𝐶 = { 𝑡 ∣ ∃ 𝑥𝐵 𝑡𝐶 }
9 6 7 8 3eqtr4g ( 𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 )
10 2 adantr ( ( 𝜑𝑥𝐵 ) → 𝐶 = 𝐷 )
11 10 iuneq2dv ( 𝜑 𝑥𝐵 𝐶 = 𝑥𝐵 𝐷 )
12 9 11 eqtrd ( 𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷 )