Theorem alsconv

Description: There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018)

	Ref	Expression
Assertion	alsconv	⊢ ( ∀! 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀! 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
2	1	anbi1i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )
3		df-alsc	⊢ ( ∀! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )
4		df-alsi	⊢ ( ∀! 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )
5	2 3 4	3bitr4ri	⊢ ( ∀! 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀! 𝑥 ∈ 𝐴 𝜑 )