Metamath Proof Explorer


Theorem elintabOLD

Description: Obsolete version of elintab as of 17-Jan-2025. (Contributed by NM, 30-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis elintab.ex AV
Assertion elintabOLD Ax|φxφAx

Proof

Step Hyp Ref Expression
1 elintab.ex AV
2 1 elint Ax|φyyx|φAy
3 nfsab1 xyx|φ
4 nfv xAy
5 3 4 nfim xyx|φAy
6 nfv yφAx
7 eleq1w y=xyx|φxx|φ
8 abid xx|φφ
9 7 8 bitrdi y=xyx|φφ
10 eleq2w y=xAyAx
11 9 10 imbi12d y=xyx|φAyφAx
12 5 6 11 cbvalv1 yyx|φAyxφAx
13 2 12 bitri Ax|φxφAx