Theorem ecopqsi

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

	Ref	Expression
Hypotheses	ecopqsi.1	$$⊢R\in \mathrm{V}$$
	ecopqsi.2	$$⊢S=\left(A\times A\right)/R$$
Assertion	ecopqsi	$$⊢\left(B\in A\wedge C\in A\right)\to \left[⟨B,C⟩\right]R\in S$$

Proof

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