Metamath Proof Explorer

Theorem equcomiv

Description: Weaker form of equcomi with a disjoint variable condition on x , y . This is an intermediate step and equcomi is fully recovered later. (Contributed by BJ, 7-Dec-2020)

Ref Expression
Assertion equcomiv x = y y = x


Step Hyp Ref Expression
1 equid x = x
2 ax7v2 x = y x = x y = x
3 1 2 mpi x = y y = x