Metamath Proof Explorer


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