Metamath Proof Explorer


Theorem elopaelxpOLD

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 x y | ψ A V × V

Proof

Step Hyp Ref Expression
1 simpl A = x y ψ A = x y
2 1 2eximi x y A = x y ψ x y A = x y
3 elopab A x y | ψ x y A = x y ψ
4 elvv A V × V x y A = x y
5 2 3 4 3imtr4i A x y | ψ A V × V