ac6s2

Description: Generalization of the Axiom of Choice to classes. Slightly strengthened version of ac6s3 . (Contributed by NM, 29-Sep-2006)

	Ref	Expression
Hypotheses	ac6s.1	$⊢ A \in V$
	ac6s.2	$⊢ y = f (x) \to (φ \leftrightarrow ψ)$
Assertion	ac6s2	$⊢ \forall x \in A \exists y φ \to \exists f (f Fn A \land \forall x \in A ψ)$

Step	Hyp	Ref	Expression
1		ac6s.1	$⊢ A \in V$
2		ac6s.2	$⊢ y = f (x) \to (φ \leftrightarrow ψ)$
3		rexv	$⊢ \exists y \in V φ \leftrightarrow \exists y φ$
4	3	ralbii	$⊢ \forall x \in A \exists y \in V φ \leftrightarrow \forall x \in A \exists y φ$
5	1 2	ac6s	$⊢ \forall x \in A \exists y \in V φ \to \exists f (f : A ⟶ V \land \forall x \in A ψ)$
6		ffn	$⊢ f : A ⟶ V \to f Fn A$
7	6	anim1i	$⊢ (f : A ⟶ V \land \forall x \in A ψ) \to (f Fn A \land \forall x \in A ψ)$
8	7	eximi	$⊢ \exists f (f : A ⟶ V \land \forall x \in A ψ) \to \exists f (f Fn A \land \forall x \in A ψ)$
9	5 8	syl	$⊢ \forall x \in A \exists y \in V φ \to \exists f (f Fn A \land \forall x \in A ψ)$
10	4 9	sylbir	$⊢ \forall x \in A \exists y φ \to \exists f (f Fn A \land \forall x \in A ψ)$

Metamath Proof Explorer