Description: Obsolete version of f1osetex as of 8-Aug-2024. (Contributed by AV, 30-Mar-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | permsetexOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapex | ||
2 | 1 | anidms | |
3 | f1of | ||
4 | 3 | ss2abi | |
5 | 4 | a1i | |
6 | 2 5 | ssexd |