ecinxp

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

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

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

Metamath Proof Explorer