Theorem fr0

Description: Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993)

	Ref	Expression
Assertion	fr0	|- R Fr (/)

Proof

Step	Hyp	Ref	Expression
1		dffr2	|- ( R Fr (/) <-> A. x ( ( x C_ (/) /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )
2		ss0	|- ( x C_ (/) -> x = (/) )
3	2	a1d	|- ( x C_ (/) -> ( -. E. y e. x { z e. x | z R y } = (/) -> x = (/) ) )
4	3	necon1ad	|- ( x C_ (/) -> ( x =/= (/) -> E. y e. x { z e. x | z R y } = (/) ) )
5	4	imp	|- ( ( x C_ (/) /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) )
6	1 5	mpgbir	|- R Fr (/)