Metamath Proof Explorer

Theorem elidinxp

Description: Characterization of the elements of the intersection of the identity relation with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elidinxp 
|- ( C e. ( _I i^i ( A X. B ) ) <-> E. x e. ( A i^i B ) C = <. x , x >. )

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( x e. B <-> E. y e. B y = x )
2 1 anbi2ci 
 |-  ( ( x e. B /\ C = <. x , x >. ) <-> ( C = <. x , x >. /\ E. y e. B y = x ) )
3 r19.42v 
 |-  ( E. y e. B ( C = <. x , x >. /\ y = x ) <-> ( C = <. x , x >. /\ E. y e. B y = x ) )
4 opeq2 
 |-  ( x = y -> <. x , x >. = <. x , y >. )
5 4 equcoms 
 |-  ( y = x -> <. x , x >. = <. x , y >. )
6 5 eqeq2d 
 |-  ( y = x -> ( C = <. x , x >. <-> C = <. x , y >. ) )
7 6 pm5.32ri 
 |-  ( ( C = <. x , x >. /\ y = x ) <-> ( C = <. x , y >. /\ y = x ) )
8 vex 
 |-  y e. _V
9 8 ideq 
 |-  ( x _I y <-> x = y )
10 df-br 
 |-  ( x _I y <-> <. x , y >. e. _I )
11 equcom 
 |-  ( x = y <-> y = x )
12 9 10 11 3bitr3i 
 |-  ( <. x , y >. e. _I <-> y = x )
13 12 anbi2i 
 |-  ( ( C = <. x , y >. /\ <. x , y >. e. _I ) <-> ( C = <. x , y >. /\ y = x ) )
14 7 13 bitr4i 
 |-  ( ( C = <. x , x >. /\ y = x ) <-> ( C = <. x , y >. /\ <. x , y >. e. _I ) )
15 14 rexbii 
 |-  ( E. y e. B ( C = <. x , x >. /\ y = x ) <-> E. y e. B ( C = <. x , y >. /\ <. x , y >. e. _I ) )
16 2 3 15 3bitr2i 
 |-  ( ( x e. B /\ C = <. x , x >. ) <-> E. y e. B ( C = <. x , y >. /\ <. x , y >. e. _I ) )
17 16 rexbii 
 |-  ( E. x e. A ( x e. B /\ C = <. x , x >. ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. _I ) )
18 rexin 
 |-  ( E. x e. ( A i^i B ) C = <. x , x >. <-> E. x e. A ( x e. B /\ C = <. x , x >. ) )
19 elinxp 
 |-  ( C e. ( _I i^i ( A X. B ) ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. _I ) )
20 17 18 19 3bitr4ri 
 |-  ( C e. ( _I i^i ( A X. B ) ) <-> E. x e. ( A i^i B ) C = <. x , x >. )