qseq2

Description: Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995)

		Ref	Expression
	Assertion	qseq2	$⊢ A = B \to C / A = C / B$

Step	Hyp	Ref	Expression
1		eceq2	$⊢ A = B \to [x] A = [x] B$
2	1	eqeq2d	$⊢ A = B \to (y = [x] A \leftrightarrow y = [x] B)$
3	2	rexbidv	$⊢ A = B \to (\exists x \in C y = [x] A \leftrightarrow \exists x \in C y = [x] B)$
4	3	abbidv	$⊢ A = B \to \{y \| \exists x \in C y = [x] A\} = \{y \| \exists x \in C y = [x] B\}$
5		df-qs	$⊢ C / A = \{y \| \exists x \in C y = [x] A\}$
6		df-qs	$⊢ C / B = \{y \| \exists x \in C y = [x] B\}$
7	4 5 6	3eqtr4g	$⊢ A = B \to C / A = C / B$

Metamath Proof Explorer