Metamath Proof Explorer


Theorem dfdisjALTV3

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV3 . (Contributed by Peter Mazsa, 28-Jul-2021)

Ref Expression
Assertion dfdisjALTV3 Disj R u v x u R x v R x u = v Rel R

Proof

Step Hyp Ref Expression
1 dfdisjALTV2 Disj R R -1 I Rel R
2 cosscnvssid3 R -1 I u v x u R x v R x u = v
3 2 anbi1i R -1 I Rel R u v x u R x v R x u = v Rel R
4 1 3 bitri Disj R u v x u R x v R x u = v Rel R