prtlem18

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

Step	Hyp	Ref	Expression
1		prtlem18.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
2		rspe	$⊢ (v \in A \land (z \in v \land w \in v)) \to \exists v \in A (z \in v \land w \in v)$
3	2	expr	$⊢ (v \in A \land z \in v) \to (w \in v \to \exists v \in A (z \in v \land w \in v))$
4	1	prtlem13	$⊢ z \underset{˙}{\sim} w \leftrightarrow \exists v \in A (z \in v \land w \in v)$
5	3 4	imbitrrdi	$⊢ (v \in A \land z \in v) \to (w \in v \to z \underset{˙}{\sim} w)$
6	5	a1i	$⊢ Prt A \to ((v \in A \land z \in v) \to (w \in v \to z \underset{˙}{\sim} w))$
7	1	prtlem13	$⊢ z \underset{˙}{\sim} w \leftrightarrow \exists p \in A (z \in p \land w \in p)$
8		prtlem17	$⊢ Prt A \to ((v \in A \land z \in v) \to (\exists p \in A (z \in p \land w \in p) \to w \in v))$
9	7 8	syl7bi	$⊢ Prt A \to ((v \in A \land z \in v) \to (z \underset{˙}{\sim} w \to w \in v))$
10	6 9	impbidd	$⊢ Prt A \to ((v \in A \land z \in v) \to (w \in v \leftrightarrow z \underset{˙}{\sim} w))$

Metamath Proof Explorer