Theorem seeq1

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

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

Proof

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