This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } = (/) )