Metamath Proof Explorer


Theorem prtlem19

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem18.1 ˙=xy|uAxuyu
Assertion prtlem19 PrtAvAzvv=z˙

Proof

Step Hyp Ref Expression
1 prtlem18.1 ˙=xy|uAxuyu
2 1 prtlem18 PrtAvAzvwvz˙w
3 2 imp PrtAvAzvwvz˙w
4 vex wV
5 vex zV
6 4 5 elec wz˙z˙w
7 3 6 bitr4di PrtAvAzvwvwz˙
8 7 eqrdv PrtAvAzvv=z˙
9 8 ex PrtAvAzvv=z˙