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

Metamath Proof Explorer

Theorem ecopqsi

Description: "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996)

Step	Hyp	Ref	Expression
1		ecopqsi.1	$⊢ R \in V$
2		ecopqsi.2	$⊢ S = (A \times A) / R$
3		opelxpi	$⊢ (B \in A \land C \in A) \to ⟨B, C⟩ \in (A \times A)$
4	1	ecelqsi	$⊢ ⟨B, C⟩ \in (A \times A) \to [⟨B, C⟩] R \in ((A \times A) / R)$
5	4 2	eleqtrrdi	$⊢ ⟨B, C⟩ \in (A \times A) \to [⟨B, C⟩] R \in S$
6	3 5	syl	$⊢ (B \in A \land C \in A) \to [⟨B, C⟩] R \in S$