This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem optoclOLD

Description: Obsolete version of optocl as of 29-Dec-2025. (Contributed by NM, 5-Mar-1995) (Proof modification is discouraged.) (New usage is discouraged.)

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 optoclOLD 
|- ( 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 imbitrid 
 |-  ( <. 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 )