Theorem bnj69

Description: Existence of a minimal element in certain classes: if R is well-founded and set-like on A , then every nonempty subclass of A has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj69	|- ( ( R _FrSe A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x )

Proof

Step	Hyp	Ref	Expression
1		biid	|- ( ( R _FrSe A /\ B C_ A /\ B =/= (/) ) <-> ( R _FrSe A /\ B C_ A /\ B =/= (/) ) )
2		biid	|- ( ( x e. B /\ y e. B /\ y R x ) <-> ( x e. B /\ y e. B /\ y R x ) )
3		biid	|- ( A. y e. B -. y R x <-> A. y e. B -. y R x )
4	1 2 3	bnj1189	|- ( ( R _FrSe A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x )