Metamath Proof Explorer


Theorem dfse3

Description: Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion dfse3 R Se A x A Pred R A x V

Proof

Step Hyp Ref Expression
1 dfse2 R Se A x A A R -1 x V
2 df-pred Pred R A x = A R -1 x
3 2 eleq1i Pred R A x V A R -1 x V
4 3 ralbii x A Pred R A x V x A A R -1 x V
5 1 4 bitr4i R Se A x A Pred R A x V