Metamath Proof Explorer


Theorem brrangeg

Description: Closed form of brrange . (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Assertion brrangeg AVBWA𝖱𝖺𝗇𝗀𝖾BB=ranA

Proof

Step Hyp Ref Expression
1 breq1 a=Aa𝖱𝖺𝗇𝗀𝖾bA𝖱𝖺𝗇𝗀𝖾b
2 rneq a=Arana=ranA
3 2 eqeq2d a=Ab=ranab=ranA
4 1 3 bibi12d a=Aa𝖱𝖺𝗇𝗀𝖾bb=ranaA𝖱𝖺𝗇𝗀𝖾bb=ranA
5 breq2 b=BA𝖱𝖺𝗇𝗀𝖾bA𝖱𝖺𝗇𝗀𝖾B
6 eqeq1 b=Bb=ranAB=ranA
7 5 6 bibi12d b=BA𝖱𝖺𝗇𝗀𝖾bb=ranAA𝖱𝖺𝗇𝗀𝖾BB=ranA
8 vex aV
9 vex bV
10 8 9 brrange a𝖱𝖺𝗇𝗀𝖾bb=rana
11 4 7 10 vtocl2g AVBWA𝖱𝖺𝗇𝗀𝖾BB=ranA