Metamath Proof Explorer

Theorem f1oabexg

Description: The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008)

Ref Expression
Hypothesis f1oabexg.1 ⊢ F = f | f : A ⟶ 1-1 onto B ∧ φ
Assertion f1oabexg ⊢ A ∈ C ∧ B ∈ D → F ∈ V

Proof

Step Hyp Ref Expression
1 f1oabexg.1 ⊢ F = f | f : A ⟶ 1-1 onto B ∧ φ
2 f1of ⊢ f : A ⟶ 1-1 onto B → f : A ⟶ B
3 2 anim1i ⊢ f : A ⟶ 1-1 onto B ∧ φ → f : A ⟶ B ∧ φ
4 3 ss2abi ⊢ f | f : A ⟶ 1-1 onto B ∧ φ ⊆ f | f : A ⟶ B ∧ φ
5 eqid ⊢ f | f : A ⟶ B ∧ φ = f | f : A ⟶ B ∧ φ
6 5 fabexg ⊢ A ∈ C ∧ B ∈ D → f | f : A ⟶ B ∧ φ ∈ V
7 ssexg ⊢ f | f : A ⟶ 1-1 onto B ∧ φ ⊆ f | f : A ⟶ B ∧ φ ∧ f | f : A ⟶ B ∧ φ ∈ V → f | f : A ⟶ 1-1 onto B ∧ φ ∈ V
8 4 6 7 sylancr ⊢ A ∈ C ∧ B ∈ D → f | f : A ⟶ 1-1 onto B ∧ φ ∈ V
9 1 8 eqeltrid ⊢ A ∈ C ∧ B ∈ D → F ∈ V