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	syl5bb	|- ( ( 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 ) )