Theorem ecopqsi

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

	Ref	Expression
Hypotheses	ecopqsi.1	|- R e. _V
	ecopqsi.2	|- S = ( ( A X. A ) /. R )
Assertion	ecopqsi	|- ( ( B e. A /\ C e. A ) -> [ <. B , C >. ] R e. S )

Proof

Step	Hyp	Ref	Expression
1		ecopqsi.1	|- R e. _V
2		ecopqsi.2	|- S = ( ( A X. A ) /. R )
3		opelxpi	|- ( ( B e. A /\ C e. A ) -> <. B , C >. e. ( A X. A ) )
4	1	ecelqsi	|- ( <. B , C >. e. ( A X. A ) -> [ <. B , C >. ] R e. ( ( A X. A ) /. R ) )
5	4 2	eleqtrrdi	|- ( <. B , C >. e. ( A X. A ) -> [ <. B , C >. ] R e. S )
6	3 5	syl	|- ( ( B e. A /\ C e. A ) -> [ <. B , C >. ] R e. S )