Metamath Proof Explorer
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29Mar1998)


Ref 
Expression 

Hypothesis 
uneq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 

Assertion 
uneq2d 
⊢ ( 𝜑 → ( 𝐶 ∪ 𝐴 ) = ( 𝐶 ∪ 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

uneq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 
2 

uneq2 
⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∪ 𝐴 ) = ( 𝐶 ∪ 𝐵 ) ) 
3 
1 2

syl 
⊢ ( 𝜑 → ( 𝐶 ∪ 𝐴 ) = ( 𝐶 ∪ 𝐵 ) ) 