Metamath Proof Explorer


Theorem frss

Description: Subset theorem for the well-founded predicate. Exercise 1 of TakeutiZaring p. 31. (Contributed by NM, 3-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion frss ABRFrBRFrA

Proof

Step Hyp Ref Expression
1 sstr2 xAABxB
2 1 com12 ABxAxB
3 2 anim1d ABxAxxBx
4 3 imim1d ABxBxyxzx¬zRyxAxyxzx¬zRy
5 4 alimdv ABxxBxyxzx¬zRyxxAxyxzx¬zRy
6 df-fr RFrBxxBxyxzx¬zRy
7 df-fr RFrAxxAxyxzx¬zRy
8 5 6 7 3imtr4g ABRFrBRFrA