Metamath Proof Explorer


Theorem ssopab2bw

Description: Equivalence of ordered pair abstraction subclass and implication. Version of ssopab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Dec-1996) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion ssopab2bw
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } <-> A. x A. y ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 nfopab1
 |-  F/_ x { <. x , y >. | ph }
2 nfopab1
 |-  F/_ x { <. x , y >. | ps }
3 1 2 nfss
 |-  F/ x { <. x , y >. | ph } C_ { <. x , y >. | ps }
4 nfopab2
 |-  F/_ y { <. x , y >. | ph }
5 nfopab2
 |-  F/_ y { <. x , y >. | ps }
6 4 5 nfss
 |-  F/ y { <. x , y >. | ph } C_ { <. x , y >. | ps }
7 ssel
 |-  ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> ( <. x , y >. e. { <. x , y >. | ph } -> <. x , y >. e. { <. x , y >. | ps } ) )
8 opabidw
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
9 opabidw
 |-  ( <. x , y >. e. { <. x , y >. | ps } <-> ps )
10 7 8 9 3imtr3g
 |-  ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> ( ph -> ps ) )
11 6 10 alrimi
 |-  ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> A. y ( ph -> ps ) )
12 3 11 alrimi
 |-  ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> A. x A. y ( ph -> ps ) )
13 ssopab2
 |-  ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } )
14 12 13 impbii
 |-  ( { <. x , y >. | ph } C_ { <. x , y >. | ps } <-> A. x A. y ( ph -> ps ) )