Theorem ecopqsi

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

	Ref	Expression
Hypotheses	ecopqsi.1	⊢ 𝑅 ∈ V
	ecopqsi.2	⊢ 𝑆 = ( ( 𝐴 × 𝐴 ) / 𝑅 )
Assertion	ecopqsi	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → [ ⟨ 𝐵 , 𝐶 ⟩ ] 𝑅 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ecopqsi.1	⊢ 𝑅 ∈ V
2		ecopqsi.2	⊢ 𝑆 = ( ( 𝐴 × 𝐴 ) / 𝑅 )
3		opelxpi	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐴 ) )
4	1	ecelqsi	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐴 ) → [ ⟨ 𝐵 , 𝐶 ⟩ ] 𝑅 ∈ ( ( 𝐴 × 𝐴 ) / 𝑅 ) )
5	4 2	eleqtrrdi	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐴 ) → [ ⟨ 𝐵 , 𝐶 ⟩ ] 𝑅 ∈ 𝑆 )
6	3 5	syl	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → [ ⟨ 𝐵 , 𝐶 ⟩ ] 𝑅 ∈ 𝑆 )