Metamath Proof Explorer


Theorem ecopqsi

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

Ref Expression
Hypotheses ecopqsi.1 R V
ecopqsi.2 S = A × A / R
Assertion ecopqsi B A C A B C R S

Proof

Step Hyp Ref Expression
1 ecopqsi.1 R V
2 ecopqsi.2 S = A × A / R
3 opelxpi B A C A B C A × A
4 1 ecelqsi B C A × A B C R A × A / R
5 4 2 eleqtrrdi B C A × A B C R S
6 3 5 syl B A C A B C R S