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 ˙=xy|uAxuyu
Assertion prtlem13 z˙wvAzvwv

Proof

Step Hyp Ref Expression
1 prtlem13.1 ˙=xy|uAxuyu
2 vex zV
3 vex wV
4 elequ2 u=vxuxv
5 elequ2 u=vyuyv
6 4 5 anbi12d u=vxuyuxvyv
7 6 cbvrexvw uAxuyuvAxvyv
8 elequ1 x=zxvzv
9 elequ1 y=wyvwv
10 8 9 bi2anan9 x=zy=wxvyvzvwv
11 10 rexbidv x=zy=wvAxvyvvAzvwv
12 7 11 syl5bb x=zy=wuAxuyuvAzvwv
13 2 3 12 1 braba z˙wvAzvwv