This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prtlem12

Description: Lemma for prtex and prter3 . (Contributed by Rodolfo Medina, 13-Oct-2010)

		Ref	Expression
	Assertion	prtlem12	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\} \to Rel \underset{˙}{\sim}$

Step	Hyp	Ref	Expression
1		relopabv	$⊢ Rel \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
2		releq	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\} \to (Rel \underset{˙}{\sim} \leftrightarrow Rel \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\})$
3	1 2	mpbiri	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\} \to Rel \underset{˙}{\sim}$