Metamath Proof Explorer


Theorem ssopab2dv

Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypothesis ssopab2dv.1 φψχ
Assertion ssopab2dv φxy|ψxy|χ

Proof

Step Hyp Ref Expression
1 ssopab2dv.1 φψχ
2 1 alrimivv φxyψχ
3 ssopab2 xyψχxy|ψxy|χ
4 2 3 syl φxy|ψxy|χ