Theorem ac6mapd

Description: Axiom of choice equivalent, deduction form. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypotheses	ac6mapd.1	|- ( y = ( f ` x ) -> ( ps <-> ch ) )
	ac6mapd.2	|- ( ph -> A e. V )
	ac6mapd.3	|- ( ph -> B e. W )
	ac6mapd.4	|- ( ( ph /\ x e. A ) -> E. y e. B ps )
Assertion	ac6mapd	|- ( ph -> E. f e. ( B ^m A ) A. x e. A ch )

Proof

Step	Hyp	Ref	Expression
1		ac6mapd.1	|- ( y = ( f ` x ) -> ( ps <-> ch ) )
2		ac6mapd.2	|- ( ph -> A e. V )
3		ac6mapd.3	|- ( ph -> B e. W )
4		ac6mapd.4	|- ( ( ph /\ x e. A ) -> E. y e. B ps )
5	4	ralrimiva	|- ( ph -> A. x e. A E. y e. B ps )
6	1	ac6sg	|- ( A e. V -> ( A. x e. A E. y e. B ps -> E. f ( f : A --> B /\ A. x e. A ch ) ) )
7	2 5 6	sylc	|- ( ph -> E. f ( f : A --> B /\ A. x e. A ch ) )
8	3 2	elmapd	|- ( ph -> ( f e. ( B ^m A ) <-> f : A --> B ) )
9	8	biimprd	|- ( ph -> ( f : A --> B -> f e. ( B ^m A ) ) )
10	9	anim1d	|- ( ph -> ( ( f : A --> B /\ A. x e. A ch ) -> ( f e. ( B ^m A ) /\ A. x e. A ch ) ) )
11	10	eximdv	|- ( ph -> ( E. f ( f : A --> B /\ A. x e. A ch ) -> E. f ( f e. ( B ^m A ) /\ A. x e. A ch ) ) )
12	7 11	mpd	|- ( ph -> E. f ( f e. ( B ^m A ) /\ A. x e. A ch ) )
13		df-rex	|- ( E. f e. ( B ^m A ) A. x e. A ch <-> E. f ( f e. ( B ^m A ) /\ A. x e. A ch ) )
14	12 13	sylibr	|- ( ph -> E. f e. ( B ^m A ) A. x e. A ch )