Metamath Proof Explorer

Theorem alsraln0

Description: The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and A is not empty. (Contributed by Peter Mazsa, 28-Nov-2018) (Revised by David A. Wheeler, 15-Jul-2026)

Ref Expression
Assertion alsraln0 
|- ( AE x ( x e. A -> ph ) <-> ( A. x e. A ph /\ A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 alsralrex 
 |-  ( AE x ( x e. A -> ph ) <-> ( A. x e. A ph /\ E. x e. A ph ) )
2 rexn0 
 |-  ( E. x e. A ph -> A =/= (/) )
3 2 a1i 
 |-  ( A. x e. A ph -> ( E. x e. A ph -> A =/= (/) ) )
4 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph )
5 4 expcom 
 |-  ( A. x e. A ph -> ( A =/= (/) -> E. x e. A ph ) )
6 3 5 impbid 
 |-  ( A. x e. A ph -> ( E. x e. A ph <-> A =/= (/) ) )
7 6 pm5.32i 
 |-  ( ( A. x e. A ph /\ E. x e. A ph ) <-> ( A. x e. A ph /\ A =/= (/) ) )
8 1 7 bitri 
 |-  ( AE x ( x e. A -> ph ) <-> ( A. x e. A ph /\ A =/= (/) ) )