Theorem ecinxp

Description: Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Assertion	ecinxp	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to \left[B\right]R=\left[B\right]\left(R\cap \left(A\times A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to B\in A$$
2	1	snssd	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to \left\{B\right\}\subseteq A$$
3		dfss2	$$⊢\left\{B\right\}\subseteq A\leftrightarrow \left\{B\right\}\cap A=\left\{B\right\}$$
4	2 3	sylib	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to \left\{B\right\}\cap A=\left\{B\right\}$$
5	4	imaeq2d	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\cap A\right]=R\left[\left\{B\right\}\right]$$
6	5	ineq1d	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\cap A\right]\cap A=R\left[\left\{B\right\}\right]\cap A$$
7		imass2	$$⊢\left\{B\right\}\subseteq A\to R\left[\left\{B\right\}\right]\subseteq R\left[A\right]$$
8	2 7	syl	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\right]\subseteq R\left[A\right]$$
9		simpl	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[A\right]\subseteq A$$
10	8 9	sstrd	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\right]\subseteq A$$
11		dfss2	$$⊢R\left[\left\{B\right\}\right]\subseteq A\leftrightarrow R\left[\left\{B\right\}\right]\cap A=R\left[\left\{B\right\}\right]$$
12	10 11	sylib	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\right]\cap A=R\left[\left\{B\right\}\right]$$
13	6 12	eqtr2d	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\right]=R\left[\left\{B\right\}\cap A\right]\cap A$$
14		imainrect	$$⊢\left(R\cap \left(A\times A\right)\right)\left[\left\{B\right\}\right]=R\left[\left\{B\right\}\cap A\right]\cap A$$
15	13 14	eqtr4di	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to R\left[\left\{B\right\}\right]=\left(R\cap \left(A\times A\right)\right)\left[\left\{B\right\}\right]$$
16		df-ec	$$⊢\left[B\right]R=R\left[\left\{B\right\}\right]$$
17		df-ec	$$⊢\left[B\right]\left(R\cap \left(A\times A\right)\right)=\left(R\cap \left(A\times A\right)\right)\left[\left\{B\right\}\right]$$
18	15 16 17	3eqtr4g	$$⊢\left(R\left[A\right]\subseteq A\wedge B\in A\right)\to \left[B\right]R=\left[B\right]\left(R\cap \left(A\times A\right)\right)$$