Metamath Proof Explorer


Theorem ac4c

Description: Equivalent of Axiom of Choice (class version). (Contributed by NM, 10-Feb-1997)

Ref Expression
Hypothesis ac4c.1 AV
Assertion ac4c fxAxfxx

Proof

Step Hyp Ref Expression
1 ac4c.1 AV
2 raleq y=AxyxfxxxAxfxx
3 2 exbidv y=AfxyxfxxfxAxfxx
4 ac4 fxyxfxx
5 1 3 4 vtocl fxAxfxx