Metamath Proof Explorer


Theorem elrid

Description: Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022) (Proof shortened by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elrid A I X x X A = x x

Proof

Step Hyp Ref Expression
1 df-res I X = I X × V
2 1 eleq2i A I X A I X × V
3 elidinxp A I X × V x X V A = x x
4 inv1 X V = X
5 4 rexeqi x X V A = x x x X A = x x
6 2 3 5 3bitri A I X x X A = x x