Theorem ac6mapd

Description: Axiom of choice equivalent, deduction form. (Contributed by Thierry Arnoux, 13-Oct-2025) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypotheses	ac6mapd.1	$$⊢y=f\left(x\right)\to \left(\psi \leftrightarrow \chi \right)$$
	ac6mapd.2	$$⊢\phi \to A\in V$$
	ac6mapd.3	$$⊢\phi \to B\in W$$
	ac6mapd.4	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in B\psi$$
Assertion	ac6mapd	$$⊢\phi \to \exists f\in \left(B^A\right)\forall x\in A\chi$$

Proof

Step	Hyp	Ref	Expression
1		ac6mapd.1	$$⊢y=f\left(x\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		ac6mapd.2	$$⊢\phi \to A\in V$$
3		ac6mapd.3	$$⊢\phi \to B\in W$$
4		ac6mapd.4	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in B\psi$$
5	4	ralrimiva	$$⊢\phi \to \forall x\in A\exists y\in B\psi$$
6	1	ac6	$$⊢\left(A\in V\wedge B\in W\wedge \forall x\in A\exists y\in B\psi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\chi \right)$$
7	2 3 5 6	syl3anc	$$⊢\phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\chi \right)$$
8	3 2	elmapd	$$⊢\phi \to \left(f\in \left(B^A\right)\leftrightarrow f:A⟶B\right)$$
9	8	biimprd	$$⊢\phi \to \left(f:A⟶B\to f\in \left(B^A\right)\right)$$
10	9	anim1d	$$⊢\phi \to \left(\left(f:A⟶B\wedge \forall x\in A\chi \right)\to \left(f\in \left(B^A\right)\wedge \forall x\in A\chi \right)\right)$$
11	10	eximdv	$$⊢\phi \to \left(\exists f\left(f:A⟶B\wedge \forall x\in A\chi \right)\to \exists f\left(f\in \left(B^A\right)\wedge \forall x\in A\chi \right)\right)$$
12	7 11	mpd	$$⊢\phi \to \exists f\left(f\in \left(B^A\right)\wedge \forall x\in A\chi \right)$$
13		df-rex	$$⊢\exists f\in \left(B^A\right)\forall x\in A\chi \leftrightarrow \exists f\left(f\in \left(B^A\right)\wedge \forall x\in A\chi \right)$$
14	12 13	sylibr	$$⊢\phi \to \exists f\in \left(B^A\right)\forall x\in A\chi$$