Metamath Proof Explorer


Definition df-cnvrefs

Description: Define the class of all converse reflexive sets, see the comment of df-ssr . It is used only by df-cnvrefrels . (Contributed by Peter Mazsa, 22-Jul-2019)

Ref Expression
Assertion df-cnvrefs
|- CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnvrefs
 |-  CnvRefs
1 vx
 |-  x
2 cid
 |-  _I
3 1 cv
 |-  x
4 3 cdm
 |-  dom x
5 3 crn
 |-  ran x
6 4 5 cxp
 |-  ( dom x X. ran x )
7 2 6 cin
 |-  ( _I i^i ( dom x X. ran x ) )
8 cssr
 |-  _S
9 8 ccnv
 |-  `' _S
10 3 6 cin
 |-  ( x i^i ( dom x X. ran x ) )
11 7 10 9 wbr
 |-  ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) )
12 11 1 cab
 |-  { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) }
13 0 12 wceq
 |-  CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) }