Metamath Proof Explorer


Theorem rankelg

Description: The membership relation is inherited by the rank function. Closed form of rankel . (Contributed by Scott Fenton, 16-Jul-2015)

Ref Expression
Assertion rankelg B V A B rank A rank B

Proof

Step Hyp Ref Expression
1 eleq2 y = B A y A B
2 fveq2 y = B rank y = rank B
3 2 eleq2d y = B rank A rank y rank A rank B
4 1 3 imbi12d y = B A y rank A rank y A B rank A rank B
5 vex y V
6 5 rankel A y rank A rank y
7 4 6 vtoclg B V A B rank A rank B
8 7 imp B V A B rank A rank B