Metamath Proof Explorer

Theorem brrelex2i

Description: The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015)

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


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