Theorem ac6s6f

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018)

	Ref	Expression
Hypotheses	ac6s6f.1	⊢ 𝐴 ∈ V
	ac6s6f.2	⊢ Ⅎ 𝑦 𝜓
	ac6s6f.3	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
	ac6s6f.4	⊢ Ⅎ 𝑥 𝐴
Assertion	ac6s6f	⊢ ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ac6s6f.1	⊢ 𝐴 ∈ V
2		ac6s6f.2	⊢ Ⅎ 𝑦 𝜓
3		ac6s6f.3	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
4		ac6s6f.4	⊢ Ⅎ 𝑥 𝐴
5	1	isseti	⊢ ∃ 𝑧 𝑧 = 𝐴
6		vex	⊢ 𝑧 ∈ V
7	2 6 3	ac6s6	⊢ ∃ 𝑓 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 )
8	5 7	exan	⊢ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ ∃ 𝑓 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) )
9		exdistr	⊢ ( ∃ 𝑧 ∃ 𝑓 ( 𝑧 = 𝐴 ∧ ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ ∃ 𝑓 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) ) )
10	8 9	mpbir	⊢ ∃ 𝑧 ∃ 𝑓 ( 𝑧 = 𝐴 ∧ ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) )
11		nfcv	⊢ Ⅎ 𝑥 𝑧
12	11 4	raleqf	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) ) )
13	12	biimpa	⊢ ( ( 𝑧 = 𝐴 ∧ ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) ) → ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) )
14	13	2eximi	⊢ ( ∃ 𝑧 ∃ 𝑓 ( 𝑧 = 𝐴 ∧ ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → 𝜓 ) ) → ∃ 𝑧 ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) )
15		ax5e	⊢ ( ∃ 𝑧 ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) )
16	10 14 15	mp2b	⊢ ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 )