Description: Obsolete version of elopaelxp as of 11-Dec-2024. (Contributed by Alexander van der Vekens, 23-Jun-2018) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elopaelxpOLD | |- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl | |- ( ( A = <. x , y >. /\ ps ) -> A = <. x , y >. ) |
|
| 2 | 1 | 2eximi | |- ( E. x E. y ( A = <. x , y >. /\ ps ) -> E. x E. y A = <. x , y >. ) |
| 3 | elopab | |- ( A e. { <. x , y >. | ps } <-> E. x E. y ( A = <. x , y >. /\ ps ) ) |
|
| 4 | elvv | |- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. ) |
|
| 5 | 2 3 4 | 3imtr4i | |- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) ) |