Theorem prtlem11

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Assertion	prtlem11	$$⊢B\in D\to \left(C\in A\to \left(B=\left[C\right]\underset{\dot{}}{\sim }\to B\in \left(A/\underset{\dot{}}{\sim }\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eceq1	$$⊢x=C\to \left[x\right]\underset{\dot{}}{\sim }=\left[C\right]\underset{\dot{}}{\sim }$$
2	1	rspceeqv	$$⊢\left(C\in A\wedge B=\left[C\right]\underset{\dot{}}{\sim }\right)\to \exists x\in AB=\left[x\right]\underset{\dot{}}{\sim }$$
3		elqsg	$$⊢B\in D\to \left(B\in \left(A/\underset{\dot{}}{\sim }\right)\leftrightarrow \exists x\in AB=\left[x\right]\underset{\dot{}}{\sim }\right)$$
4	2 3	syl5ibr	$$⊢B\in D\to \left(\left(C\in A\wedge B=\left[C\right]\underset{\dot{}}{\sim }\right)\to B\in \left(A/\underset{\dot{}}{\sim }\right)\right)$$
5	4	expd	$$⊢B\in D\to \left(C\in A\to \left(B=\left[C\right]\underset{\dot{}}{\sim }\to B\in \left(A/\underset{\dot{}}{\sim }\right)\right)\right)$$