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 ) )