Metamath Proof Explorer


Theorem dfantisymrel5

Description: Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024)

Ref Expression
Assertion dfantisymrel5 AntisymRel R x y x R y y R x x = y Rel R

Proof

Step Hyp Ref Expression
1 df-antisymrel AntisymRel R CnvRefRel R R -1 Rel R
2 relcnv Rel R -1
3 relin2 Rel R -1 Rel R R -1
4 2 3 ax-mp Rel R R -1
5 dfcnvrefrel5 CnvRefRel R R -1 x y x R R -1 y x = y Rel R R -1
6 4 5 mpbiran2 CnvRefRel R R -1 x y x R R -1 y x = y
7 brcnvin x V y V x R R -1 y x R y y R x
8 7 el2v x R R -1 y x R y y R x
9 8 imbi1i x R R -1 y x = y x R y y R x x = y
10 9 2albii x y x R R -1 y x = y x y x R y y R x x = y
11 6 10 bitri CnvRefRel R R -1 x y x R y y R x x = y
12 1 11 bianbi AntisymRel R x y x R y y R x x = y Rel R