Theorem ac6sg

Description: ac6s with sethood as antecedent. (Contributed by FL, 3-Aug-2009)

	Ref	Expression
Hypothesis	ac6sg.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ac6sg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ac6sg.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
2		raleq	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
3		feq2	⊢ ( 𝑧 = 𝐴 → ( 𝑓 : 𝑧 ⟶ 𝐵 ↔ 𝑓 : 𝐴 ⟶ 𝐵 ) )
4		raleq	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
5	3 4	anbi12d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑓 : 𝑧 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 𝜓 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
6	5	exbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
7	2 6	imbi12d	⊢ ( 𝑧 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) )
8		vex	⊢ 𝑧 ∈ V
9	8 1	ac6s	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 𝜓 ) )
10	7 9	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )