Theorem ac6mapd

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

	Ref	Expression
Hypotheses	ac6mapd.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜓 ↔ 𝜒 ) )
	ac6mapd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ac6mapd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	ac6mapd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion	ac6mapd	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∀ 𝑥 ∈ 𝐴 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		ac6mapd.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜓 ↔ 𝜒 ) )
2		ac6mapd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ac6mapd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		ac6mapd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝜓 )
5	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
6	1	ac6sg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) )
7	2 5 6	sylc	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
8	3 2	elmapd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐵 ) )
9	8	biimprd	⊢ ( 𝜑 → ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ) )
10	9	anim1d	⊢ ( 𝜑 → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) )
11	10	eximdv	⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) → ∃ 𝑓 ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) )
12	7 11	mpd	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
13		df-rex	⊢ ( ∃ 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
14	12 13	sylibr	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∀ 𝑥 ∈ 𝐴 𝜒 )