Metamath Proof Explorer


Theorem prtlem12

Description: Lemma for prtex and prter3 . (Contributed by Rodolfo Medina, 13-Oct-2010)

Ref Expression
Assertion prtlem12 ˙=xy|uAxuyuRel˙

Proof

Step Hyp Ref Expression
1 relopabv Relxy|uAxuyu
2 releq ˙=xy|uAxuyuRel˙Relxy|uAxuyu
3 1 2 mpbiri ˙=xy|uAxuyuRel˙