Theorem optocl

Description: Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995)

	Ref	Expression
Hypotheses	optocl.1	|- D = ( B X. C )
	optocl.2	|- ( <. x , y >. = A -> ( ph <-> ps ) )
	optocl.3	|- ( ( x e. B /\ y e. C ) -> ph )
Assertion	optocl	|- ( A e. D -> ps )

Proof

Step	Hyp	Ref	Expression
1		optocl.1	|- D = ( B X. C )
2		optocl.2	|- ( <. x , y >. = A -> ( ph <-> ps ) )
3		optocl.3	|- ( ( x e. B /\ y e. C ) -> ph )
4		elxp3	|- ( A e. ( B X. C ) <-> E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) )
5		opelxp	|- ( <. x , y >. e. ( B X. C ) <-> ( x e. B /\ y e. C ) )
6	5 3	sylbi	|- ( <. x , y >. e. ( B X. C ) -> ph )
7	6 2	syl5ib	|- ( <. x , y >. = A -> ( <. x , y >. e. ( B X. C ) -> ps ) )
8	7	imp	|- ( ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) -> ps )
9	8	exlimivv	|- ( E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) -> ps )
10	4 9	sylbi	|- ( A e. ( B X. C ) -> ps )
11	10 1	eleq2s	|- ( A e. D -> ps )