# Metamath Proof Explorer

## Theorem dffr3

Description: Alternate definition of well-founded relation. Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dffr3
`|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )`

### Proof

Step Hyp Ref Expression
1 dffr2
` |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )`
2 iniseg
` |-  ( y e. _V -> ( `' R " { y } ) = { z | z R y } )`
3 2 elv
` |-  ( `' R " { y } ) = { z | z R y }`
4 3 ineq2i
` |-  ( x i^i ( `' R " { y } ) ) = ( x i^i { z | z R y } )`
5 dfrab3
` |-  { z e. x | z R y } = ( x i^i { z | z R y } )`
6 4 5 eqtr4i
` |-  ( x i^i ( `' R " { y } ) ) = { z e. x | z R y }`
7 6 eqeq1i
` |-  ( ( x i^i ( `' R " { y } ) ) = (/) <-> { z e. x | z R y } = (/) )`
8 7 rexbii
` |-  ( E. y e. x ( x i^i ( `' R " { y } ) ) = (/) <-> E. y e. x { z e. x | z R y } = (/) )`
9 8 imbi2i
` |-  ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )`
10 9 albii
` |-  ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )`
11 1 10 bitr4i
` |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )`