Metamath Proof Explorer

Theorem brab2dd

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Hypotheses brab2dd.1 
|- ( ph -> R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ps ) } )
brab2dd.2 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
brab2dd.3 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( x e. C /\ y e. D ) <-> ( A e. U /\ B e. V ) ) )
Assertion brab2dd 
|- ( ph -> ( A R B <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 brab2dd.1 
 |-  ( ph -> R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ps ) } )
2 brab2dd.2 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
3 brab2dd.3 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( x e. C /\ y e. D ) <-> ( A e. U /\ B e. V ) ) )
4 df-br 
 |-  ( A R B <-> <. A , B >. e. R )
5 1 eleq2d 
 |-  ( ph -> ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ps ) } ) )
6 4 5 bitrid 
 |-  ( ph -> ( A R B <-> <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ps ) } ) )
7 elopab 
 |-  ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ps ) } <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) )
8 6 7 bitrdi 
 |-  ( ph -> ( A R B <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) ) )
9 simpl 
 |-  ( ( ph /\ ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) ) -> ph )
10 eqcom 
 |-  ( <. x , y >. = <. A , B >. <-> <. A , B >. = <. x , y >. )
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 11 12 opth 
 |-  ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) )
14 10 13 sylbb1 
 |-  ( <. A , B >. = <. x , y >. -> ( x = A /\ y = B ) )
15 14 ad2antrl 
 |-  ( ( ph /\ ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) ) -> ( x = A /\ y = B ) )
16 simprrl 
 |-  ( ( ph /\ ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) ) -> ( x e. C /\ y e. D ) )
17 3 biimpa 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ ( x e. C /\ y e. D ) ) -> ( A e. U /\ B e. V ) )
18 9 15 16 17 syl21anc 
 |-  ( ( ph /\ ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) ) -> ( A e. U /\ B e. V ) )
19 18 ex 
 |-  ( ph -> ( ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) -> ( A e. U /\ B e. V ) ) )
20 19 exlimdvv 
 |-  ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) -> ( A e. U /\ B e. V ) ) )
21 20 imp 
 |-  ( ( ph /\ E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) ) -> ( A e. U /\ B e. V ) )
22 simprl 
 |-  ( ( ph /\ ( ( A e. U /\ B e. V ) /\ ch ) ) -> ( A e. U /\ B e. V ) )
23 simprl 
 |-  ( ( ph /\ ( A e. U /\ B e. V ) ) -> A e. U )
24 simprr 
 |-  ( ( ph /\ ( A e. U /\ B e. V ) ) -> B e. V )
25 3 2 anbi12d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( ( x e. C /\ y e. D ) /\ ps ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
26 25 adantlr 
 |-  ( ( ( ph /\ ( A e. U /\ B e. V ) ) /\ ( x = A /\ y = B ) ) -> ( ( ( x e. C /\ y e. D ) /\ ps ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
27 23 24 26 copsex2dv 
 |-  ( ( ph /\ ( A e. U /\ B e. V ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
28 21 22 27 bibiad 
 |-  ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. C /\ y e. D ) /\ ps ) ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
29 8 28 bitrd 
 |-  ( ph -> ( A R B <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )