Theorem axac10

Description: Characterization of choice similar to dffin1-5 . (Contributed by Stefan O'Rear, 6-Jan-2015)

	Ref	Expression
Assertion	axac10	⊢ ( ≈ “ On ) = V

Proof

Step	Hyp	Ref	Expression
1		axac3	⊢ CHOICE
2		dfac10b	⊢ ( CHOICE ↔ ( ≈ “ On ) = V )
3	1 2	mpbi	⊢ ( ≈ “ On ) = V