This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions f1oiOLD
Description: Obsolete version of f1oi as of 10-Feb-2026. (Contributed by NM , 30-Apr-1998) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
f1oiOLD ⊢ I ↾ A : A ⟶ 1-1 onto A
Proof
Step
Hyp
Ref
Expression
1
fnresi ⊢ I ↾ A Fn A
2
cnvresid ⊢ I ↾ A -1 = I ↾ A
3
2
fneq1i ⊢ I ↾ A -1 Fn A ↔ I ↾ A Fn A
4
1 3
mpbir ⊢ I ↾ A -1 Fn A
5
dff1o4 ⊢ I ↾ A : A ⟶ 1-1 onto A ↔ I ↾ A Fn A ∧ I ↾ A -1 Fn A
6
1 4 5
mpbir2an ⊢ I ↾ A : A ⟶ 1-1 onto A