Theorem epfrc

Description: A subset of a well-founded class has a minimal element. (Contributed by NM, 17-Feb-2004) (Revised by David Abernethy, 22-Feb-2011)

	Ref	Expression
Hypothesis	epfrc.1	|- B e. _V
Assertion	epfrc	|- ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		epfrc.1	|- B e. _V
2	1	frc	|- ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y _E x } = (/) )
3		dfin5	|- ( B i^i x ) = { y e. B | y e. x }
4		epel	|- ( y _E x <-> y e. x )
5	4	rabbii	|- { y e. B | y _E x } = { y e. B | y e. x }
6	3 5	eqtr4i	|- ( B i^i x ) = { y e. B | y _E x }
7	6	eqeq1i	|- ( ( B i^i x ) = (/) <-> { y e. B | y _E x } = (/) )
8	7	rexbii	|- ( E. x e. B ( B i^i x ) = (/) <-> E. x e. B { y e. B | y _E x } = (/) )
9	2 8	sylibr	|- ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )