Metamath Proof Explorer

Theorem ssoprab2b

Description: Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by FL, 6-Nov-2013) (Proof shortened by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfoprab1 
 |-  F/_ x { <. <. x , y >. , z >. | ph }
2 nfoprab1 
 |-  F/_ x { <. <. x , y >. , z >. | ps }
3 1 2 nfss 
 |-  F/ x { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps }
4 nfoprab2 
 |-  F/_ y { <. <. x , y >. , z >. | ph }
5 nfoprab2 
 |-  F/_ y { <. <. x , y >. , z >. | ps }
6 4 5 nfss 
 |-  F/ y { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps }
7 nfoprab3 
 |-  F/_ z { <. <. x , y >. , z >. | ph }
8 nfoprab3 
 |-  F/_ z { <. <. x , y >. , z >. | ps }
9 7 8 nfss 
 |-  F/ z { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps }
10 ssel 
 |-  ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } -> ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } -> <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ps } ) )
11 oprabid 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
12 oprabid 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ps } <-> ps )
13 10 11 12 3imtr3g 
 |-  ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } -> ( ph -> ps ) )
14 9 13 alrimi 
 |-  ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } -> A. z ( ph -> ps ) )
15 6 14 alrimi 
 |-  ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } -> A. y A. z ( ph -> ps ) )
16 3 15 alrimi 
 |-  ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } -> A. x A. y A. z ( ph -> ps ) )
17 ssoprab2 
 |-  ( A. x A. y A. z ( ph -> ps ) -> { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } )
18 16 17 impbii 
 |-  ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } <-> A. x A. y A. z ( ph -> ps ) )