Metamath Proof Explorer

Theorem cnvssb

Description: Subclass theorem for converse. (Contributed by RP, 22-Oct-2020)

Ref Expression
Assertion cnvssb 
|- ( Rel A -> ( A C_ B <-> `' A C_ `' B ) )

Proof

Step Hyp Ref Expression
1 cnvss 
 |-  ( A C_ B -> `' A C_ `' B )
2 cnvss 
 |-  ( `' A C_ `' B -> `' `' A C_ `' `' B )
3 dfrel2 
 |-  ( Rel A <-> `' `' A = A )
4 3 biimpi 
 |-  ( Rel A -> `' `' A = A )
5 4 eqcomd 
 |-  ( Rel A -> A = `' `' A )
6 5 adantr 
 |-  ( ( Rel A /\ `' `' A C_ `' `' B ) -> A = `' `' A )
7 id 
 |-  ( `' `' A C_ `' `' B -> `' `' A C_ `' `' B )
8 cnvcnvss 
 |-  `' `' B C_ B
9 7 8 sstrdi 
 |-  ( `' `' A C_ `' `' B -> `' `' A C_ B )
10 9 adantl 
 |-  ( ( Rel A /\ `' `' A C_ `' `' B ) -> `' `' A C_ B )
11 6 10 eqsstrd 
 |-  ( ( Rel A /\ `' `' A C_ `' `' B ) -> A C_ B )
12 11 ex 
 |-  ( Rel A -> ( `' `' A C_ `' `' B -> A C_ B ) )
13 2 12 syl5 
 |-  ( Rel A -> ( `' A C_ `' B -> A C_ B ) )
14 1 13 impbid2 
 |-  ( Rel A -> ( A C_ B <-> `' A C_ `' B ) )