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) (Proof shortened by AV, 9-Jun-2025)

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 elex ⊢ A ∈ C → A ∈ V
3 elex ⊢ B ∈ D → B ∈ V
4 f1of ⊢ f : A ⟶ 1-1 onto B → f : A ⟶ B
5 4 ad2antrl ⊢ A ∈ V ∧ B ∈ V ∧ f : A ⟶ 1-1 onto B ∧ φ → f : A ⟶ B
6 simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
7 simpr ⊢ A ∈ V ∧ B ∈ V → B ∈ V
8 5 6 7 fabexd ⊢ A ∈ V ∧ B ∈ V → f | f : A ⟶ 1-1 onto B ∧ φ ∈ V
9 1 8 eqeltrid ⊢ A ∈ V ∧ B ∈ V → F ∈ V
10 2 3 9 syl2an ⊢ A ∈ C ∧ B ∈ D → F ∈ V