ac5

Description: An Axiom of Choice equivalent: there exists a function f (called a choice function) with domain A that maps each nonempty member of the domain to an element of that member. Axiom AC of BellMachover p. 488. Note that the assertion that f be a function is not necessary; see ac4 . (Contributed by NM, 29-Aug-1999)

		Ref	Expression
	Hypothesis	ac5.1	$⊢ A \in V$
	Assertion	ac5	$⊢ \exists f (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x))$

Proof

Step	Hyp	Ref	Expression
1		ac5.1	$⊢ A \in V$
2		fneq2	$⊢ y = A \to (f Fn y \leftrightarrow f Fn A)$
3		raleq	$⊢ y = A \to (\forall x \in y (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in A (x \neq \emptyset \to f (x) \in x))$
4	2 3	anbi12d	$⊢ y = A \to ((f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x)))$
5	4	exbidv	$⊢ y = A \to (\exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \leftrightarrow \exists f (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x)))$
6		dfac4	$⊢ CHOICE \leftrightarrow \forall y \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))$
7	6	axaci	$⊢ \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))$
8	1 5 7	vtocl	$⊢ \exists f (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x))$

Metamath Proof Explorer

Theorem ac5

Proof