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 | |
|
Assertion | elintabOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elintab.ex | |
|
2 | 1 | elint | |
3 | nfsab1 | |
|
4 | nfv | |
|
5 | 3 4 | nfim | |
6 | nfv | |
|
7 | eleq1w | |
|
8 | abid | |
|
9 | 7 8 | bitrdi | |
10 | eleq2w | |
|
11 | 9 10 | imbi12d | |
12 | 5 6 11 | cbvalv1 | |
13 | 2 12 | bitri | |