Theorem cosseq

Description: Equality theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 9-Jan-2018)

	Ref	Expression
Assertion	cosseq	$$⊢A=B\to \wr A=\wr B$$

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢A=B\to \left(uAx\leftrightarrow uBx\right)$$
2		breq	$$⊢A=B\to \left(uAy\leftrightarrow uBy\right)$$
3	1 2	anbi12d	$$⊢A=B\to \left(\left(uAx\wedge uAy\right)\leftrightarrow \left(uBx\wedge uBy\right)\right)$$
4	3	exbidv	$$⊢A=B\to \left(\exists u\left(uAx\wedge uAy\right)\leftrightarrow \exists u\left(uBx\wedge uBy\right)\right)$$
5	4	opabbidv	$$⊢A=B\to \left\{⟨x,y⟩|\exists u\left(uAx\wedge uAy\right)\right\}=\left\{⟨x,y⟩|\exists u\left(uBx\wedge uBy\right)\right\}$$
6		df-coss	$$⊢\wr A=\left\{⟨x,y⟩|\exists u\left(uAx\wedge uAy\right)\right\}$$
7		df-coss	$$⊢\wr B=\left\{⟨x,y⟩|\exists u\left(uBx\wedge uBy\right)\right\}$$
8	5 6 7	3eqtr4g	$$⊢A=B\to \wr A=\wr B$$