Metamath Proof Explorer

Theorem cosseqd

Description: Equality theorem for the classes of cosets by A and B , deduction form. (Contributed by Peter Mazsa, 4-Nov-2019)

Ref Expression
Hypothesis cosseqd.1 
|- ( ph -> A = B )
Assertion cosseqd 
|- ( ph -> ,~ A = ,~ B )

Proof

Step Hyp Ref Expression
1 cosseqd.1 
 |-  ( ph -> A = B )
2 cosseq 
 |-  ( A = B -> ,~ A = ,~ B )
3 1 2 syl 
 |-  ( ph -> ,~ A = ,~ B )