Theorem 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	⊢ ( 𝑅 ∈ 𝐴 → ∃ 𝑓 ( 𝑓 ⊆ 𝑅 ∧ 𝑓 Fn dom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		sseq2	⊢ ( 𝑥 = 𝑅 → ( 𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑅 ) )
2		dmeq	⊢ ( 𝑥 = 𝑅 → dom 𝑥 = dom 𝑅 )
3	2	fneq2d	⊢ ( 𝑥 = 𝑅 → ( 𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑅 ) )
4	1 3	anbi12d	⊢ ( 𝑥 = 𝑅 → ( ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ( 𝑓 ⊆ 𝑅 ∧ 𝑓 Fn dom 𝑅 ) ) )
5	4	exbidv	⊢ ( 𝑥 = 𝑅 → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ 𝑅 ∧ 𝑓 Fn dom 𝑅 ) ) )
6		ac7	⊢ ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 )
7	5 6	vtoclg	⊢ ( 𝑅 ∈ 𝐴 → ∃ 𝑓 ( 𝑓 ⊆ 𝑅 ∧ 𝑓 Fn dom 𝑅 ) )