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

Metamath Proof Explorer

Theorem bnj1154

Description: Property of Fr . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bnj658	\|- ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> ( R Fr A /\ B C_ A /\ B =/= (/) ) )
2		elisset	\|- ( B e. _V -> E. b b = B )
3	2	bnj708	\|- ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. b b = B )
4		df-fr	\|- ( R Fr A <-> A. b ( ( b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) )
5	4	biimpi	\|- ( R Fr A -> A. b ( ( b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) )
6	5	19.21bi	\|- ( R Fr A -> ( ( b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) )
7	6	3impib	\|- ( ( R Fr A /\ b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x )
8		sseq1	\|- ( b = B -> ( b C_ A <-> B C_ A ) )
9		neeq1	\|- ( b = B -> ( b =/= (/) <-> B =/= (/) ) )
10	8 9	3anbi23d	\|- ( b = B -> ( ( R Fr A /\ b C_ A /\ b =/= (/) ) <-> ( R Fr A /\ B C_ A /\ B =/= (/) ) ) )
11		raleq	\|- ( b = B -> ( A. y e. b -. y R x <-> A. y e. B -. y R x ) )
12	11	rexeqbi1dv	\|- ( b = B -> ( E. x e. b A. y e. b -. y R x <-> E. x e. B A. y e. B -. y R x ) )
13	10 12	imbi12d	\|- ( b = B -> ( ( ( R Fr A /\ b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) <-> ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
14	7 13	mpbii	\|- ( b = B -> ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) )
15	3 14	bnj593	\|- ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. b ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) )
16	15	bnj937	\|- ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) )
17	1 16	mpd	\|- ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. x e. B A. y e. B -. y R x )