Theorem seeq2

Description: Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	seeq2	$$⊢A=B\to \left(R\mathrm{Se}A\leftrightarrow R\mathrm{Se}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢A=B\to B\subseteq A$$
2		sess2	$$⊢B\subseteq A\to \left(R\mathrm{Se}A\to R\mathrm{Se}B\right)$$
3	1 2	syl	$$⊢A=B\to \left(R\mathrm{Se}A\to R\mathrm{Se}B\right)$$
4		eqimss	$$⊢A=B\to A\subseteq B$$
5		sess2	$$⊢A\subseteq B\to \left(R\mathrm{Se}B\to R\mathrm{Se}A\right)$$
6	4 5	syl	$$⊢A=B\to \left(R\mathrm{Se}B\to R\mathrm{Se}A\right)$$
7	3 6	impbid	$$⊢A=B\to \left(R\mathrm{Se}A\leftrightarrow R\mathrm{Se}B\right)$$