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. y e. B -. y R x )
3	1 2	mpanl1	|- ( ( R Fr A /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
4	3	3impb	|- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x )
5		rabeq0	|- ( { y e. B | y R x } = (/) <-> A. y e. B -. y R x )
6	5	rexbii	|- ( E. x e. B { y e. B | y R x } = (/) <-> E. x e. B A. y e. B -. y R x )
7	4 6	sylibr	|- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) )