Theorem ac7

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

	Ref	Expression
Assertion	ac7	⊢ ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		df-ac	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) )
2	1	axaci	⊢ ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 )