Description: Equivalent of Axiom of Choice (class version). (Contributed by NM, 10-Feb-1997)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ac4c.1 | |
|
Assertion | ac4c | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ac4c.1 | |
|
2 | raleq | |
|
3 | 2 | exbidv | |
4 | ac4 | |
|
5 | 1 3 4 | vtocl | |