Theorem frc

Description: Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 19-Nov-2014)

	Ref	Expression
Hypothesis	frc.1	|- B e. _V
Assertion	frc	|- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) )

Proof

Step	Hyp	Ref	Expression
1		frc.1	|- B e. _V
2		fri	|- ( ( ( B e. _V /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. z e. B -. z R x )
3	1 2	mpanl1	|- ( ( R Fr A /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. z e. B -. z R x )
4	3	3impb	|- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. z e. B -. z R x )
5		breq1	|- ( y = z -> ( y R x <-> z R x ) )
6	5	rabeq0w	|- ( { y e. B | y R x } = (/) <-> A. z e. B -. z R x )
7	6	rexbii	|- ( E. x e. B { y e. B | y R x } = (/) <-> E. x e. B A. z e. B -. z R x )
8	4 7	sylibr	|- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) )