Metamath Proof Explorer


Theorem relelrnb

Description: Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015)

Ref Expression
Assertion relelrnb RelRAranRxxRA

Proof

Step Hyp Ref Expression
1 elrng AranRAranRxxRA
2 1 ibi AranRxxRA
3 relelrn RelRxRAAranR
4 3 ex RelRxRAAranR
5 4 exlimdv RelRxxRAAranR
6 2 5 impbid2 RelRAranRxxRA