This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )