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	$$⊢\phi \to A=B$$
Assertion	cosseqd	$$⊢\phi \to \wr A=\wr B$$

Proof

Step	Hyp	Ref	Expression
1		cosseqd.1	$$⊢\phi \to A=B$$
2		cosseq	$$⊢A=B\to \wr A=\wr B$$
3	1 2	syl	$$⊢\phi \to \wr A=\wr B$$