ac7g

Description: An Axiom of Choice equivalent similar to the Axiom of Choice (first form) of Enderton p. 49. (Contributed by NM, 23-Jul-2004)

		Ref	Expression
	Assertion	ac7g	$⊢ R \in A \to \exists f (f \subseteq R \land f Fn dom R)$

Step	Hyp	Ref	Expression
1		sseq2	$⊢ x = R \to (f \subseteq x \leftrightarrow f \subseteq R)$
2		dmeq	$⊢ x = R \to dom x = dom R$
3	2	fneq2d	$⊢ x = R \to (f Fn dom x \leftrightarrow f Fn dom R)$
4	1 3	anbi12d	$⊢ x = R \to ((f \subseteq x \land f Fn dom x) \leftrightarrow (f \subseteq R \land f Fn dom R))$
5	4	exbidv	$⊢ x = R \to (\exists f (f \subseteq x \land f Fn dom x) \leftrightarrow \exists f (f \subseteq R \land f Fn dom R))$
6		ac7	$⊢ \exists f (f \subseteq x \land f Fn dom x)$
7	5 6	vtoclg	$⊢ R \in A \to \exists f (f \subseteq R \land f Fn dom R)$

Metamath Proof Explorer