Metamath Proof Explorer


Theorem permsetexOLD

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 A V f | f : A 1-1 onto A V

Proof

Step Hyp Ref Expression
1 mapex A V A V f | f : A A V
2 1 anidms A V f | f : A A V
3 f1of f : A 1-1 onto A f : A A
4 3 ss2abi f | f : A 1-1 onto A f | f : A A
5 4 a1i A V f | f : A 1-1 onto A f | f : A A
6 2 5 ssexd A V f | f : A 1-1 onto A V