Metamath Proof Explorer

Theorem brrelex1i

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998)

Ref Expression
Hypothesis brrelexi.1 Rel R
Assertion brrelex1i A R B A V


Step Hyp Ref Expression
1 brrelexi.1 Rel R
2 brrelex1 Rel R A R B A V
3 1 2 mpan A R B A V