Metamath Proof Explorer

Theorem reflexg

Description: Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020)

Ref Expression
Assertion reflexg 
|- ( ( _I |` ( dom A u. ran A ) ) C_ A <-> A. x A. y ( x A y -> ( x A x /\ y A y ) ) )

Proof

Step Hyp Ref Expression
1 undmrnresiss 
 |-  ( ( _I |` ( dom A u. ran A ) ) C_ A <-> A. x A. y ( x A y -> ( x A x /\ y A y ) ) )