Metamath Proof Explorer


Theorem f1mptrn

Description: Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020)

Ref Expression
Hypotheses f1mptrn.1 φxABC
f1mptrn.2 φyC∃!xAy=B
Assertion f1mptrn φFunxAB-1

Proof

Step Hyp Ref Expression
1 f1mptrn.1 φxABC
2 f1mptrn.2 φyC∃!xAy=B
3 1 ralrimiva φxABC
4 2 ralrimiva φyC∃!xAy=B
5 eqid xAB=xAB
6 5 f1ompt xAB:A1-1 ontoCxABCyC∃!xAy=B
7 dff1o2 xAB:A1-1 ontoCxABFnAFunxAB-1ranxAB=C
8 7 simp2bi xAB:A1-1 ontoCFunxAB-1
9 6 8 sylbir xABCyC∃!xAy=BFunxAB-1
10 3 4 9 syl2anc φFunxAB-1