prtlem11

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

Step	Hyp	Ref	Expression
1		eceq1	$⊢ x = C \to [x] \underset{˙}{\sim} = [C] \underset{˙}{\sim}$
2	1	rspceeqv	$⊢ (C \in A \land B = [C] \underset{˙}{\sim}) \to \exists x \in A B = [x] \underset{˙}{\sim}$
3		elqsg	$⊢ B \in D \to (B \in (A / \underset{˙}{\sim}) \leftrightarrow \exists x \in A B = [x] \underset{˙}{\sim})$
4	2 3	imbitrrid	$⊢ B \in D \to ((C \in A \land B = [C] \underset{˙}{\sim}) \to B \in (A / \underset{˙}{\sim}))$
5	4	expd	$⊢ B \in D \to (C \in A \to (B = [C] \underset{˙}{\sim} \to B \in (A / \underset{˙}{\sim})))$

Metamath Proof Explorer