Metamath Proof Explorer

Theorem prtlem12

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

Ref Expression
Assertion prtlem12 
|- ( .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) } -> Rel .~ )

Proof

Step Hyp Ref Expression
1 relopabv 
 |-  Rel { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2 releq 
 |-  ( .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) } -> ( Rel .~ <-> Rel { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) } ) )
3 1 2 mpbiri 
 |-  ( .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) } -> Rel .~ )