Metamath Proof Explorer


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 A f f R f Fn dom R

Proof

Step Hyp Ref Expression
1 sseq2 x = R f x f 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 x f Fn dom x f R f Fn dom R
5 4 exbidv x = R f f x f Fn dom x f f R f Fn dom R
6 ac7 f f x f Fn dom x
7 5 6 vtoclg R A f f R f Fn dom R