Metamath Proof Explorer


Theorem intidOLD

Description: Obsolete version of intidg as of 18-Jan-2025. (Contributed by NM, 5-Jun-2009) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis intid.1 A V
Assertion intidOLD x | A x = A

Proof

Step Hyp Ref Expression
1 intid.1 A V
2 snex A V
3 eleq2 x = A A x A A
4 1 snid A A
5 3 4 intmin3 A V x | A x A
6 2 5 ax-mp x | A x A
7 1 elintab A x | A x x A x A x
8 id A x A x
9 7 8 mpgbir A x | A x
10 snssi A x | A x A x | A x
11 9 10 ax-mp A x | A x
12 6 11 eqssi x | A x = A