ac6gf

	Ref	Expression
Hypotheses	ac6gf.1	$⊢ Ⅎ y ψ$
	ac6gf.2	$⊢ y = f (x) \to (φ \leftrightarrow ψ)$
Assertion	ac6gf	$⊢ (A \in C \land \forall x \in A \exists y \in B φ) \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$

Step	Hyp	Ref	Expression
1		ac6gf.1	$⊢ Ⅎ y ψ$
2		ac6gf.2	$⊢ y = f (x) \to (φ \leftrightarrow ψ)$
3		cbvrexsvw	$⊢ \exists y \in B φ \leftrightarrow \exists z \in B [z/ y] φ$
4	3	ralbii	$⊢ \forall x \in A \exists y \in B φ \leftrightarrow \forall x \in A \exists z \in B [z/ y] φ$
5	1 2	sbhypf	$⊢ z = f (x) \to ([z/ y] φ \leftrightarrow ψ)$
6	5	ac6sg	$⊢ A \in C \to (\forall x \in A \exists z \in B [z/ y] φ \to \exists f (f : A ⟶ B \land \forall x \in A ψ))$
7	6	imp	$⊢ (A \in C \land \forall x \in A \exists z \in B [z/ y] φ) \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$
8	4 7	sylan2b	$⊢ (A \in C \land \forall x \in A \exists y \in B φ) \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$

Metamath Proof Explorer