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