Theorem optocl

Description: Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995) Shorten and reduce axiom usage. (Revised by TM, 29-Dec-2025)

	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		elxpi	|- ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
5	2	eqcoms	|- ( A = <. x , y >. -> ( ph <-> ps ) )
6	3 5	imbitrid	|- ( A = <. x , y >. -> ( ( x e. B /\ y e. C ) -> ps ) )
7	6	imp	|- ( ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) -> ps )
8	7	exlimivv	|- ( E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) -> ps )
9	4 8	syl	|- ( A e. ( B X. C ) -> ps )
10	9 1	eleq2s	|- ( A e. D -> ps )