Metamath Proof Explorer


Theorem elrng

Description: Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion elrng A V A ran B x x B A

Proof

Step Hyp Ref Expression
1 elrn2g A V A ran B x x A B
2 df-br x B A x A B
3 2 exbii x x B A x x A B
4 1 3 bitr4di A V A ran B x x B A