Description: One direction of ceqsalt is based on fewer assumptions and fewer axioms. It is at the same time the reverse direction of vtoclgft . Extracted from a proof of ceqsalt . (Contributed by Wolf Lammen, 25-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | ceqsal1t |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpr | ||
2 | 1 | imim2i | |
3 | 2 | com23 | |
4 | 3 | alimi | |
5 | 19.21t | ||
6 | 4 5 | imbitrid | |
7 | 6 | imp |