Metamath Proof Explorer


Theorem uneq12

Description: Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998)

Ref Expression
Assertion uneq12 ( ( 𝐴 = 𝐵𝐶 = 𝐷 ) → ( 𝐴𝐶 ) = ( 𝐵𝐷 ) )

Proof

Step Hyp Ref Expression
1 uneq1 ( 𝐴 = 𝐵 → ( 𝐴𝐶 ) = ( 𝐵𝐶 ) )
2 uneq2 ( 𝐶 = 𝐷 → ( 𝐵𝐶 ) = ( 𝐵𝐷 ) )
3 1 2 sylan9eq ( ( 𝐴 = 𝐵𝐶 = 𝐷 ) → ( 𝐴𝐶 ) = ( 𝐵𝐷 ) )