Metamath Proof Explorer


Theorem ssopab2b

Description: Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ssopab2bw when possible. (Contributed by NM, 27-Dec-1996) (Proof shortened by Mario Carneiro, 18-Nov-2016) (New usage is discouraged.)

Ref Expression
Assertion ssopab2b x y | φ x y | ψ x y φ ψ

Proof

Step Hyp Ref Expression
1 nfopab1 _ x x y | φ
2 nfopab1 _ x x y | ψ
3 1 2 nfss x x y | φ x y | ψ
4 nfopab2 _ y x y | φ
5 nfopab2 _ y x y | ψ
6 4 5 nfss y x y | φ x y | ψ
7 ssel x y | φ x y | ψ x y x y | φ x y x y | ψ
8 opabid x y x y | φ φ
9 opabid x y x y | ψ ψ
10 7 8 9 3imtr3g x y | φ x y | ψ φ ψ
11 6 10 alrimi x y | φ x y | ψ y φ ψ
12 3 11 alrimi x y | φ x y | ψ x y φ ψ
13 ssopab2 x y φ ψ x y | φ x y | ψ
14 12 13 impbii x y | φ x y | ψ x y φ ψ