prtlem19

		Ref	Expression
	Hypothesis	prtlem18.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
	Assertion	prtlem19	$⊢ Prt A \to ((v \in A \land z \in v) \to v = [z] \underset{˙}{\sim})$

Step	Hyp	Ref	Expression
1		prtlem18.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
2	1	prtlem18	$⊢ Prt A \to ((v \in A \land z \in v) \to (w \in v \leftrightarrow z \underset{˙}{\sim} w))$
3	2	imp	$⊢ (Prt A \land (v \in A \land z \in v)) \to (w \in v \leftrightarrow z \underset{˙}{\sim} w)$
4		vex	$⊢ w \in V$
5		vex	$⊢ z \in V$
6	4 5	elec	$⊢ w \in [z] \underset{˙}{\sim} \leftrightarrow z \underset{˙}{\sim} w$
7	3 6	bitr4di	$⊢ (Prt A \land (v \in A \land z \in v)) \to (w \in v \leftrightarrow w \in [z] \underset{˙}{\sim})$
8	7	eqrdv	$⊢ (Prt A \land (v \in A \land z \in v)) \to v = [z] \underset{˙}{\sim}$
9	8	ex	$⊢ Prt A \to ((v \in A \land z \in v) \to v = [z] \underset{˙}{\sim})$

Metamath Proof Explorer