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

Metamath Proof Explorer

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 )