Description: "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ecopqsi.1 | ||
ecopqsi.2 | |||
Assertion | ecopqsi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecopqsi.1 | ||
2 | ecopqsi.2 | ||
3 | opelxpi | ||
4 | 1 | ecelqsi | |
5 | 4 2 | eleqtrrdi | |
6 | 3 5 | syl |