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	|- ( R e. A -> E. f ( f C_ R /\ f Fn dom R ) )

Proof

Step	Hyp	Ref	Expression
1		sseq2	|- ( x = R -> ( f C_ x <-> f C_ R ) )
2		dmeq	|- ( x = R -> dom x = dom R )
3	2	fneq2d	|- ( x = R -> ( f Fn dom x <-> f Fn dom R ) )
4	1 3	anbi12d	|- ( x = R -> ( ( f C_ x /\ f Fn dom x ) <-> ( f C_ R /\ f Fn dom R ) ) )
5	4	exbidv	|- ( x = R -> ( E. f ( f C_ x /\ f Fn dom x ) <-> E. f ( f C_ R /\ f Fn dom R ) ) )
6		ac7	|- E. f ( f C_ x /\ f Fn dom x )
7	5 6	vtoclg	|- ( R e. A -> E. f ( f C_ R /\ f Fn dom R ) )