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

Metamath Proof Explorer

Theorem prtlem13

Description: Lemma for prter1 , prter2 , prter3 and prtex . (Contributed by Rodolfo Medina, 13-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem13.1 
|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion prtlem13 
|- ( z .~ w <-> E. v e. A ( z e. v /\ w e. v ) )

Proof

Step Hyp Ref Expression
1 prtlem13.1 
 |-  .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2 vex 
 |-  z e. _V
3 vex 
 |-  w e. _V
4 elequ2 
 |-  ( u = v -> ( x e. u <-> x e. v ) )
5 elequ2 
 |-  ( u = v -> ( y e. u <-> y e. v ) )
6 4 5 anbi12d 
 |-  ( u = v -> ( ( x e. u /\ y e. u ) <-> ( x e. v /\ y e. v ) ) )
7 6 cbvrexvw 
 |-  ( E. u e. A ( x e. u /\ y e. u ) <-> E. v e. A ( x e. v /\ y e. v ) )
8 elequ1 
 |-  ( x = z -> ( x e. v <-> z e. v ) )
9 elequ1 
 |-  ( y = w -> ( y e. v <-> w e. v ) )
10 8 9 bi2anan9 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. v /\ y e. v ) <-> ( z e. v /\ w e. v ) ) )
11 10 rexbidv 
 |-  ( ( x = z /\ y = w ) -> ( E. v e. A ( x e. v /\ y e. v ) <-> E. v e. A ( z e. v /\ w e. v ) ) )
12 7 11 bitrid 
 |-  ( ( x = z /\ y = w ) -> ( E. u e. A ( x e. u /\ y e. u ) <-> E. v e. A ( z e. v /\ w e. v ) ) )
13 2 3 12 1 braba 
 |-  ( z .~ w <-> E. v e. A ( z e. v /\ w e. v ) )