Metamath Proof Explorer

Theorem copsex2d

Description: Implicit substitution deduction for ordered pairs. (Contributed by BJ, 25-Dec-2023)

Ref Expression
Hypotheses copsex2d.xph 
|- ( ph -> A. x ph )
copsex2d.yph 
|- ( ph -> A. y ph )
copsex2d.xch 
|- ( ph -> F/ x ch )
copsex2d.ych 
|- ( ph -> F/ y ch )
copsex2d.exa 
|- ( ph -> A e. U )
copsex2d.exb 
|- ( ph -> B e. V )
copsex2d.is 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion copsex2d 
|- ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )

Proof

Step Hyp Ref Expression
1 copsex2d.xph 
 |-  ( ph -> A. x ph )
2 copsex2d.yph 
 |-  ( ph -> A. y ph )
3 copsex2d.xch 
 |-  ( ph -> F/ x ch )
4 copsex2d.ych 
 |-  ( ph -> F/ y ch )
5 copsex2d.exa 
 |-  ( ph -> A e. U )
6 copsex2d.exb 
 |-  ( ph -> B e. V )
7 copsex2d.is 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
8 elisset 
 |-  ( A e. U -> E. x x = A )
9 5 8 syl 
 |-  ( ph -> E. x x = A )
10 elisset 
 |-  ( B e. V -> E. y y = B )
11 6 10 syl 
 |-  ( ph -> E. y y = B )
12 exdistrv 
 |-  ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
13 nfe1 
 |-  F/ x E. x E. y ( <. A , B >. = <. x , y >. /\ ps )
14 13 a1i 
 |-  ( ph -> F/ x E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) )
15 14 3 nfbid 
 |-  ( ph -> F/ x ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )
16 15 19.9d 
 |-  ( ph -> ( E. x ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) ) )
17 nfe1 
 |-  F/ y E. y ( <. A , B >. = <. x , y >. /\ ps )
18 17 a1i 
 |-  ( ph -> F/ y E. y ( <. A , B >. = <. x , y >. /\ ps ) )
19 1 18 bj-nfexd 
 |-  ( ph -> F/ y E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) )
20 19 4 nfbid 
 |-  ( ph -> F/ y ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )
21 20 19.9d 
 |-  ( ph -> ( E. y ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) ) )
22 opeq12 
 |-  ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
23 copsexgw 
 |-  ( <. A , B >. = <. x , y >. -> ( ps <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) ) )
24 23 bicomd 
 |-  ( <. A , B >. = <. x , y >. -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ps ) )
25 24 eqcoms 
 |-  ( <. x , y >. = <. A , B >. -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ps ) )
26 22 25 syl 
 |-  ( ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ps ) )
27 26 adantl 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ps ) )
28 27 7 bitrd 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )
29 28 ex 
 |-  ( ph -> ( ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) ) )
30 2 21 29 bj-exlimd 
 |-  ( ph -> ( E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) ) )
31 1 16 30 bj-exlimd 
 |-  ( ph -> ( E. x E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) ) )
32 12 31 biimtrrid 
 |-  ( ph -> ( ( E. x x = A /\ E. y y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) ) )
33 9 11 32 mp2and 
 |-  ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )