Metamath Proof Explorer


Theorem uneq12

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

Ref Expression
Assertion uneq12 A=BC=DAC=BD

Proof

Step Hyp Ref Expression
1 uneq1 A=BAC=BC
2 uneq2 C=DBC=BD
3 1 2 sylan9eq A=BC=DAC=BD