Metamath Proof Explorer

Theorem relssresb

Description: Biconditional form of relssres , to replace it. (Contributed by BJ, 8-Nov-2026)

Ref Expression
Assertion relssresb 
|- ( ( Rel A /\ dom A C_ B ) <-> ( A |` B ) = A )

Proof

Step Hyp Ref Expression
1 relssdmrnb 
 |-  ( Rel A <-> A C_ ( dom A X. ran A ) )
2 simpl 
 |-  ( ( A C_ ( dom A X. ran A ) /\ dom A C_ B ) -> A C_ ( dom A X. ran A ) )
3 simpr 
 |-  ( ( A C_ ( dom A X. ran A ) /\ dom A C_ B ) -> dom A C_ B )
4 ssv 
 |-  ran A C_ _V
5 xpss12 
 |-  ( ( dom A C_ B /\ ran A C_ _V ) -> ( dom A X. ran A ) C_ ( B X. _V ) )
6 3 4 5 sylancl 
 |-  ( ( A C_ ( dom A X. ran A ) /\ dom A C_ B ) -> ( dom A X. ran A ) C_ ( B X. _V ) )
7 2 6 sstrd 
 |-  ( ( A C_ ( dom A X. ran A ) /\ dom A C_ B ) -> A C_ ( B X. _V ) )
8 1 7 sylanb 
 |-  ( ( Rel A /\ dom A C_ B ) -> A C_ ( B X. _V ) )
9 id 
 |-  ( A C_ ( B X. _V ) -> A C_ ( B X. _V ) )
10 xpss 
 |-  ( B X. _V ) C_ ( _V X. _V )
11 9 10 sstrdi 
 |-  ( A C_ ( B X. _V ) -> A C_ ( _V X. _V ) )
12 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
13 11 12 sylibr 
 |-  ( A C_ ( B X. _V ) -> Rel A )
14 dmss 
 |-  ( A C_ ( B X. _V ) -> dom A C_ dom ( B X. _V ) )
15 dmxpss 
 |-  dom ( B X. _V ) C_ B
16 14 15 sstrdi 
 |-  ( A C_ ( B X. _V ) -> dom A C_ B )
17 13 16 jca 
 |-  ( A C_ ( B X. _V ) -> ( Rel A /\ dom A C_ B ) )
18 8 17 impbii 
 |-  ( ( Rel A /\ dom A C_ B ) <-> A C_ ( B X. _V ) )
19 bj-resssxp 
 |-  ( ( A |` B ) = A <-> A C_ ( B X. _V ) )
20 18 19 bitr4i 
 |-  ( ( Rel A /\ dom A C_ B ) <-> ( A |` B ) = A )