Metamath Proof Explorer

Theorem friOLD

Description: Obsolete version of fri as of 16-Nov-2024. (Contributed by NM, 18-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-fr 
 |-  ( R Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) )
2 sseq1 
 |-  ( z = B -> ( z C_ A <-> B C_ A ) )
3 neeq1 
 |-  ( z = B -> ( z =/= (/) <-> B =/= (/) ) )
4 2 3 anbi12d 
 |-  ( z = B -> ( ( z C_ A /\ z =/= (/) ) <-> ( B C_ A /\ B =/= (/) ) ) )
5 raleq 
 |-  ( z = B -> ( A. y e. z -. y R x <-> A. y e. B -. y R x ) )
6 5 rexeqbi1dv 
 |-  ( z = B -> ( E. x e. z A. y e. z -. y R x <-> E. x e. B A. y e. B -. y R x ) )
7 4 6 imbi12d 
 |-  ( z = B -> ( ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) <-> ( ( B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
8 7 spcgv 
 |-  ( B e. C -> ( A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) -> ( ( B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
9 1 8 syl5bi 
 |-  ( B e. C -> ( R Fr A -> ( ( B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
10 9 imp31 
 |-  ( ( ( B e. C /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )