Metamath Proof Explorer


Theorem xrneq1

Description: Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020)

Ref Expression
Assertion xrneq1 A=BAC=BC

Proof

Step Hyp Ref Expression
1 coeq2 A=B1stV×V-1A=1stV×V-1B
2 1 ineq1d A=B1stV×V-1A2ndV×V-1C=1stV×V-1B2ndV×V-1C
3 df-xrn AC=1stV×V-1A2ndV×V-1C
4 df-xrn BC=1stV×V-1B2ndV×V-1C
5 2 3 4 3eqtr4g A=BAC=BC