Metamath Proof Explorer

Theorem bj-idreseqb

Description: Characterization for two classes to be related under the restricted identity relation. (Contributed by BJ, 24-Dec-2023)

Ref Expression
Assertion bj-idreseqb 
|- ( A ( _I |` C ) B <-> ( A e. C /\ A = B ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( _I |` C )
2 1 brrelex12i 
 |-  ( A ( _I |` C ) B -> ( A e. _V /\ B e. _V ) )
3 simpl 
 |-  ( ( A e. C /\ A = B ) -> A e. C )
4 3 elexd 
 |-  ( ( A e. C /\ A = B ) -> A e. _V )
5 eleq1 
 |-  ( A = B -> ( A e. C <-> B e. C ) )
6 5 biimpac 
 |-  ( ( A e. C /\ A = B ) -> B e. C )
7 6 elexd 
 |-  ( ( A e. C /\ A = B ) -> B e. _V )
8 4 7 jca 
 |-  ( ( A e. C /\ A = B ) -> ( A e. _V /\ B e. _V ) )
9 brres 
 |-  ( B e. _V -> ( A ( _I |` C ) B <-> ( A e. C /\ A _I B ) ) )
10 9 adantl 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A ( _I |` C ) B <-> ( A e. C /\ A _I B ) ) )
11 eqeq12 
 |-  ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) )
12 df-id 
 |-  _I = { <. x , y >. | x = y }
13 11 12 brabga 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A _I B <-> A = B ) )
14 13 anbi2d 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( A e. C /\ A _I B ) <-> ( A e. C /\ A = B ) ) )
15 10 14 bitrd 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A ( _I |` C ) B <-> ( A e. C /\ A = B ) ) )
16 2 8 15 pm5.21nii 
 |-  ( A ( _I |` C ) B <-> ( A e. C /\ A = B ) )