Metamath Proof Explorer

Theorem ac2

Description: Axiom of Choice equivalent. By using restricted quantifiers, we can express the Axiom of Choice with a single explicit conjunction. (If you want to figure it out, the rewritten equivalent ac3 is easier to understand.) Note: aceq0 shows the logical equivalence to ax-ac . (New usage is discouraged.) (Contributed by NM, 18-Jul-1996)

		Ref	Expression
	Assertion	ac2	\|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )

Proof

Step	Hyp	Ref	Expression
1		ax-ac	\|- E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) )
2		aceq0	\|- ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) )
3	1 2	mpbir	\|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )

Step

Hyp

Ref

Expression

ax-ac

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

aceq0

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

1 2

mpbir

 |-  E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )