Metamath Proof Explorer
Description: Equality inference for the union of two classes. (Contributed by NM, 12Aug2004) (Proof shortened by Eric Schmidt, 26Jan2007)


Ref 
Expression 

Hypotheses 
uneq1i.1 
$${\u22a2}{A}={B}$$ 


uneq12i.2 
$${\u22a2}{C}={D}$$ 

Assertion 
uneq12i 
$${\u22a2}{A}\cup {C}={B}\cup {D}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

uneq1i.1 
$${\u22a2}{A}={B}$$ 
2 

uneq12i.2 
$${\u22a2}{C}={D}$$ 
3 

uneq12 
$${\u22a2}\left({A}={B}\wedge {C}={D}\right)\to {A}\cup {C}={B}\cup {D}$$ 
4 
1 2 3

mp2an 
$${\u22a2}{A}\cup {C}={B}\cup {D}$$ 