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	|- ( A! x ( x e. A -> ph ) <-> A! x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2	1	anbi1i	|- ( ( A. x e. A ph /\ E. x x e. A ) <-> ( A. x ( x e. A -> ph ) /\ E. x x e. A ) )
3		df-alsc	|- ( A! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )
4		df-alsi	|- ( A! x ( x e. A -> ph ) <-> ( A. x ( x e. A -> ph ) /\ E. x x e. A ) )
5	2 3 4	3bitr4ri	|- ( A! x ( x e. A -> ph ) <-> A! x e. A ph )