Metamath Proof Explorer

Theorem eqoprab2bw

Description: Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Jan-2017) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion eqoprab2bw 
|- ( { <. <. x , y >. , z >. | ph } = { <. <. 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 oprabidw 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
12 oprabidw 
 |-  ( <. <. 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 ) )
19 2 1 nfss 
 |-  F/ x { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph }
20 5 4 nfss 
 |-  F/ y { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph }
21 8 7 nfss 
 |-  F/ z { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph }
22 ssel 
 |-  ( { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } -> ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ps } -> <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } ) )
23 22 12 11 3imtr3g 
 |-  ( { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } -> ( ps -> ph ) )
24 21 23 alrimi 
 |-  ( { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } -> A. z ( ps -> ph ) )
25 20 24 alrimi 
 |-  ( { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } -> A. y A. z ( ps -> ph ) )
26 19 25 alrimi 
 |-  ( { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } -> A. x A. y A. z ( ps -> ph ) )
27 ssoprab2 
 |-  ( A. x A. y A. z ( ps -> ph ) -> { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } )
28 26 27 impbii 
 |-  ( { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } <-> A. x A. y A. z ( ps -> ph ) )
29 18 28 anbi12i 
 |-  ( ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } /\ { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } ) <-> ( A. x A. y A. z ( ph -> ps ) /\ A. x A. y A. z ( ps -> ph ) ) )
30 eqss 
 |-  ( { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } <-> ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } /\ { <. <. x , y >. , z >. | ps } C_ { <. <. x , y >. , z >. | ph } ) )
31 2albiim 
 |-  ( A. y A. z ( ph <-> ps ) <-> ( A. y A. z ( ph -> ps ) /\ A. y A. z ( ps -> ph ) ) )
32 31 albii 
 |-  ( A. x A. y A. z ( ph <-> ps ) <-> A. x ( A. y A. z ( ph -> ps ) /\ A. y A. z ( ps -> ph ) ) )
33 19.26 
 |-  ( A. x ( A. y A. z ( ph -> ps ) /\ A. y A. z ( ps -> ph ) ) <-> ( A. x A. y A. z ( ph -> ps ) /\ A. x A. y A. z ( ps -> ph ) ) )
34 32 33 bitri 
 |-  ( A. x A. y A. z ( ph <-> ps ) <-> ( A. x A. y A. z ( ph -> ps ) /\ A. x A. y A. z ( ps -> ph ) ) )
35 29 30 34 3bitr4i 
 |-  ( { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } <-> A. x A. y A. z ( ph <-> ps ) )