Metamath Proof Explorer

Theorem ac8prim

Description: ac8 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025)

		Ref	Expression
	Assertion	ac8prim	\|- ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5prim	\|- ( CHOICE <-> A. x ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
2	1	axaci	\|- ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) )

Step

Hyp

Ref

Expression

dfac5prim

 |-  ( CHOICE <-> A. x ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )

axaci

 |-  ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) )