Metamath Proof Explorer

Theorem relcoels

Description: Coelements on A is a relation. (Contributed by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion relcoels 
|- Rel ~ A

Proof

Step Hyp Ref Expression
1 relcoss 
 |-  Rel ,~ ( `' _E |` A )
2 df-coels 
 |-  ~ A = ,~ ( `' _E |` A )
3 2 releqi 
 |-  ( Rel ~ A <-> Rel ,~ ( `' _E |` A ) )
4 1 3 mpbir 
 |-  Rel ~ A