Theorem ecoptocl

Description: Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995)

	Ref	Expression
Hypotheses	ecoptocl.1	|- S = ( ( B X. C ) /. R )
	ecoptocl.2	|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )
	ecoptocl.3	|- ( ( x e. B /\ y e. C ) -> ph )
Assertion	ecoptocl	|- ( A e. S -> ps )

Proof

Step	Hyp	Ref	Expression
1		ecoptocl.1	|- S = ( ( B X. C ) /. R )
2		ecoptocl.2	|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )
3		ecoptocl.3	|- ( ( x e. B /\ y e. C ) -> ph )
4		elqsi	|- ( A e. ( ( B X. C ) /. R ) -> E. z e. ( B X. C ) A = [ z ] R )
5		eqid	|- ( B X. C ) = ( B X. C )
6		eceq1	|- ( <. x , y >. = z -> [ <. x , y >. ] R = [ z ] R )
7	6	eqeq2d	|- ( <. x , y >. = z -> ( A = [ <. x , y >. ] R <-> A = [ z ] R ) )
8	7	imbi1d	|- ( <. x , y >. = z -> ( ( A = [ <. x , y >. ] R -> ps ) <-> ( A = [ z ] R -> ps ) ) )
9	2	eqcoms	|- ( A = [ <. x , y >. ] R -> ( ph <-> ps ) )
10	3 9	syl5ibcom	|- ( ( x e. B /\ y e. C ) -> ( A = [ <. x , y >. ] R -> ps ) )
11	5 8 10	optocl	|- ( z e. ( B X. C ) -> ( A = [ z ] R -> ps ) )
12	11	rexlimiv	|- ( E. z e. ( B X. C ) A = [ z ] R -> ps )
13	4 12	syl	|- ( A e. ( ( B X. C ) /. R ) -> ps )
14	13 1	eleq2s	|- ( A e. S -> ps )