Theorem qusin

Description: Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	qusin.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusin.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusin.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
	qusin.r	$$⊢\phi \to R\in Z$$
	qusin.s	$$⊢\phi \to \underset{\dot{}}{\sim }\left[V\right]\subseteq V$$
Assertion	qusin	$$⊢\phi \to U=R{/}_{𝑠}\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		qusin.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusin.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusin.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
4		qusin.r	$$⊢\phi \to R\in Z$$
5		qusin.s	$$⊢\phi \to \underset{\dot{}}{\sim }\left[V\right]\subseteq V$$
6		ecinxp	$$⊢\left(\underset{\dot{}}{\sim }\left[V\right]\subseteq V\wedge x\in V\right)\to \left[x\right]\underset{\dot{}}{\sim }=\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)$$
7	5 6	sylan	$$⊢\left(\phi \wedge x\in V\right)\to \left[x\right]\underset{\dot{}}{\sim }=\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)$$
8	7	mpteq2dva	$$⊢\phi \to \left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in V⟼\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)\right)$$
9	8	oveq1d	$$⊢\phi \to \left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right){“}_{𝑠}R=\left(x\in V⟼\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)\right){“}_{𝑠}R$$
10		eqid	$$⊢\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
11	1 2 10 3 4	qusval	$$⊢\phi \to U=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right){“}_{𝑠}R$$
12		eqidd	$$⊢\phi \to R{/}_{𝑠}\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)=R{/}_{𝑠}\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)$$
13		eqid	$$⊢\left(x\in V⟼\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)\right)=\left(x\in V⟼\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)\right)$$
14		inex1g	$$⊢\underset{\dot{}}{\sim }\in W\to \underset{\dot{}}{\sim }\cap \left(V\times V\right)\in \mathrm{V}$$
15	3 14	syl	$$⊢\phi \to \underset{\dot{}}{\sim }\cap \left(V\times V\right)\in \mathrm{V}$$
16	12 2 13 15 4	qusval	$$⊢\phi \to R{/}_{𝑠}\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)=\left(x\in V⟼\left[x\right]\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)\right){“}_{𝑠}R$$
17	9 11 16	3eqtr4d	$$⊢\phi \to U=R{/}_{𝑠}\left(\underset{\dot{}}{\sim }\cap \left(V\times V\right)\right)$$