Metamath Proof Explorer

Theorem dfac2

Description: Axiom of Choice (first form) of Enderton p. 49 corresponds to our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC, but the Axiom of Regularity is used (by applying dfac2b ). (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

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

Proof

Step	Hyp	Ref	Expression
1		dfac2b	\|- ( CHOICE -> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
2		dfac2a	\|- ( A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> CHOICE )
3	1 2	impbii	\|- ( CHOICE <-> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )

Step

Hyp

Ref

Expression

dfac2b

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

dfac2a

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

1 2

impbii

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