Theorem alsc2d

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

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

Proof

Step	Hyp	Ref	Expression
1		alsc2d.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	simprd	$$⊢\phi \to \exists xx\in A$$