Metamath Proof Explorer


Definition df-pred

Description: Define the predecessor class of a binary relation. This is the class of all elements y of A such that y R X (see elpred ). (Contributed by Scott Fenton, 29-Jan-2011)

Ref Expression
Assertion df-pred Pred R A X = A R -1 X

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 cX class X
3 1 0 2 cpred class Pred R A X
4 0 ccnv class R -1
5 2 csn class X
6 4 5 cima class R -1 X
7 1 6 cin class A R -1 X
8 3 7 wceq wff Pred R A X = A R -1 X