Metamath Proof Explorer
Description: Inference adding union to the left in a class equality. (Contributed by NM, 30Aug1993)


Ref 
Expression 

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

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

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

uneq2 
$${\u22a2}{A}={B}\to {C}\cup {A}={C}\cup {B}$$ 
3 
1 2

axmp 
$${\u22a2}{C}\cup {A}={C}\cup {B}$$ 