Theorem bnj1185

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj1185.1	|- ( ph -> E. z e. B A. w e. B -. w R z )
Assertion	bnj1185	|- ( ph -> E. x e. B A. y e. B -. y R x )

Proof

Step	Hyp	Ref	Expression
1		bnj1185.1	|- ( ph -> E. z e. B A. w e. B -. w R z )
2		breq1	|- ( w = y -> ( w R z <-> y R z ) )
3	2	notbid	|- ( w = y -> ( -. w R z <-> -. y R z ) )
4	3	cbvralvw	|- ( A. w e. B -. w R z <-> A. y e. B -. y R z )
5	4	rexbii	|- ( E. z e. B A. w e. B -. w R z <-> E. z e. B A. y e. B -. y R z )
6	1 5	sylib	|- ( ph -> E. z e. B A. y e. B -. y R z )
7		eleq1w	|- ( z = x -> ( z e. B <-> x e. B ) )
8		breq2	|- ( z = x -> ( y R z <-> y R x ) )
9	8	notbid	|- ( z = x -> ( -. y R z <-> -. y R x ) )
10	9	ralbidv	|- ( z = x -> ( A. y e. B -. y R z <-> A. y e. B -. y R x ) )
11	7 10	anbi12d	|- ( z = x -> ( ( z e. B /\ A. y e. B -. y R z ) <-> ( x e. B /\ A. y e. B -. y R x ) ) )
12	11	cbvexvw	|- ( E. z ( z e. B /\ A. y e. B -. y R z ) <-> E. x ( x e. B /\ A. y e. B -. y R x ) )
13		df-rex	|- ( E. z e. B A. y e. B -. y R z <-> E. z ( z e. B /\ A. y e. B -. y R z ) )
14		df-rex	|- ( E. x e. B A. y e. B -. y R x <-> E. x ( x e. B /\ A. y e. B -. y R x ) )
15	12 13 14	3bitr4ri	|- ( E. x e. B A. y e. B -. y R x <-> E. z e. B A. y e. B -. y R z )
16	6 15	sylibr	|- ( ph -> E. x e. B A. y e. B -. y R x )