This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axac2

Description: Derive ax-ac2 from ax-ac . (Contributed by NM, 19-Dec-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion axac2 
|- E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac2a 
 |-  ( A. x E. y A. z e. x ( z =/= (/) -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) -> CHOICE )
2 ac3 
 |-  E. y A. z e. x ( z =/= (/) -> E! v e. z E. u e. y ( z e. u /\ v e. u ) )
3 1 2 mpg 
 |-  CHOICE
4 dfackm 
 |-  ( CHOICE <-> A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )
5 3 4 mpbi 
 |-  A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) )
6 5 spi 
 |-  E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) )