Metamath Proof Explorer

Theorem rexopabb

Description: Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023)

Ref Expression
Hypotheses rexopabb.o 
|- O = { <. x , y >. | ph }
rexopabb.p 
|- ( o = <. x , y >. -> ( ps <-> ch ) )
Assertion rexopabb 
|- ( E. o e. O ps <-> E. x E. y ( ph /\ ch ) )

Proof

Step Hyp Ref Expression
1 rexopabb.o 
 |-  O = { <. x , y >. | ph }
2 rexopabb.p 
 |-  ( o = <. x , y >. -> ( ps <-> ch ) )
3 1 rexeqi 
 |-  ( E. o e. O ps <-> E. o e. { <. x , y >. | ph } ps )
4 elopab 
 |-  ( o e. { <. x , y >. | ph } <-> E. x E. y ( o = <. x , y >. /\ ph ) )
5 simprr 
 |-  ( ( ps /\ ( o = <. x , y >. /\ ph ) ) -> ph )
6 2 biimpd 
 |-  ( o = <. x , y >. -> ( ps -> ch ) )
7 6 adantr 
 |-  ( ( o = <. x , y >. /\ ph ) -> ( ps -> ch ) )
8 7 impcom 
 |-  ( ( ps /\ ( o = <. x , y >. /\ ph ) ) -> ch )
9 5 8 jca 
 |-  ( ( ps /\ ( o = <. x , y >. /\ ph ) ) -> ( ph /\ ch ) )
10 9 ex 
 |-  ( ps -> ( ( o = <. x , y >. /\ ph ) -> ( ph /\ ch ) ) )
11 10 2eximdv 
 |-  ( ps -> ( E. x E. y ( o = <. x , y >. /\ ph ) -> E. x E. y ( ph /\ ch ) ) )
12 11 impcom 
 |-  ( ( E. x E. y ( o = <. x , y >. /\ ph ) /\ ps ) -> E. x E. y ( ph /\ ch ) )
13 4 12 sylanb 
 |-  ( ( o e. { <. x , y >. | ph } /\ ps ) -> E. x E. y ( ph /\ ch ) )
14 13 rexlimiva 
 |-  ( E. o e. { <. x , y >. | ph } ps -> E. x E. y ( ph /\ ch ) )
15 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
16 nfv 
 |-  F/ x ps
17 15 16 nfrex 
 |-  F/ x E. o e. { <. x , y >. | ph } ps
18 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
19 nfv 
 |-  F/ y ps
20 18 19 nfrex 
 |-  F/ y E. o e. { <. x , y >. | ph } ps
21 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
22 opex 
 |-  <. x , y >. e. _V
23 22 2 sbcie 
 |-  ( [. <. x , y >. / o ]. ps <-> ch )
24 rspesbca 
 |-  ( ( <. x , y >. e. { <. x , y >. | ph } /\ [. <. x , y >. / o ]. ps ) -> E. o e. { <. x , y >. | ph } ps )
25 21 23 24 syl2anbr 
 |-  ( ( ph /\ ch ) -> E. o e. { <. x , y >. | ph } ps )
26 20 25 exlimi 
 |-  ( E. y ( ph /\ ch ) -> E. o e. { <. x , y >. | ph } ps )
27 17 26 exlimi 
 |-  ( E. x E. y ( ph /\ ch ) -> E. o e. { <. x , y >. | ph } ps )
28 14 27 impbii 
 |-  ( E. o e. { <. x , y >. | ph } ps <-> E. x E. y ( ph /\ ch ) )
29 3 28 bitri 
 |-  ( E. o e. O ps <-> E. x E. y ( ph /\ ch ) )