qsresid

Description: Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020)

		Ref	Expression
	Assertion	qsresid	$⊢ A / ({R ↾}_{A}) = A / R$

Step	Hyp	Ref	Expression
1		elecreseq	$⊢ v \in A \to [v] ({R ↾}_{A}) = [v] R$
2	1	eqeq2d	$⊢ v \in A \to (u = [v] ({R ↾}_{A}) \leftrightarrow u = [v] R)$
3	2	rexbiia	$⊢ \exists v \in A u = [v] ({R ↾}_{A}) \leftrightarrow \exists v \in A u = [v] R$
4	3	abbii	$⊢ \{u \| \exists v \in A u = [v] ({R ↾}_{A})\} = \{u \| \exists v \in A u = [v] R\}$
5		df-qs	$⊢ A / ({R ↾}_{A}) = \{u \| \exists v \in A u = [v] ({R ↾}_{A})\}$
6		df-qs	$⊢ A / R = \{u \| \exists v \in A u = [v] R\}$
7	4 5 6	3eqtr4i	$⊢ A / ({R ↾}_{A}) = A / R$

Metamath Proof Explorer