Metamath Proof Explorer

Theorem f1oabexgOLD

Description: Obsolete version of f1oabexg as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis f1oabexg.1 ⊢ F = f | f : A ⟶ 1-1 onto B ∧ φ
Assertion f1oabexgOLD ⊢ 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