Theorem alsc1d

Description: Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018)

	Ref	Expression
Hypothesis	alsc1d.1	$$⊢\phi \to \forall !x\in A\psi$$
Assertion	alsc1d	$$⊢\phi \to \forall x\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		alsc1d.1	$$⊢\phi \to \forall !x\in A\psi$$
2		df-alsc	$$⊢\forall !x\in A\psi \leftrightarrow \left(\forall x\in A\psi \wedge \exists xx\in A\right)$$
3	1 2	sylib	$$⊢\phi \to \left(\forall x\in A\psi \wedge \exists xx\in A\right)$$
4	3	simpld	$$⊢\phi \to \forall x\in A\psi$$