Metamath Proof Explorer


Theorem dffr4

Description: Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion dffr4 RFrAxxAxyxPredRxy=

Proof

Step Hyp Ref Expression
1 dffr3 RFrAxxAxyxxR-1y=
2 df-pred PredRxy=xR-1y
3 2 eqeq1i PredRxy=xR-1y=
4 3 rexbii yxPredRxy=yxxR-1y=
5 4 imbi2i xAxyxPredRxy=xAxyxxR-1y=
6 5 albii xxAxyxPredRxy=xxAxyxxR-1y=
7 1 6 bitr4i RFrAxxAxyxPredRxy=