Metamath Proof Explorer

Theorem refrelid

Description: Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021)

Ref Expression
Assertion refrelid 
|- RefRel _I

Proof

Step Hyp Ref Expression
1 ssid 
 |-  ( _I i^i ( dom _I X. ran _I ) ) C_ ( _I i^i ( dom _I X. ran _I ) )
2 reli 
 |-  Rel _I
3 df-refrel 
 |-  ( RefRel _I <-> ( ( _I i^i ( dom _I X. ran _I ) ) C_ ( _I i^i ( dom _I X. ran _I ) ) /\ Rel _I ) )
4 1 2 3 mpbir2an 
 |-  RefRel _I