Theorem 2alsraln0id

Description: Nested general "all some" quantifiers with class membership as their antecedents, for the same class A : ph holds for every x and every y in A , and A is not empty. (Contributed by Peter Mazsa, 28-May-2019) (Revised by David A. Wheeler, 15-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		2alsraln0	|- ( AE x ( x e. A -> AE y ( y e. A -> ph ) ) <-> ( A. x e. A A. y e. A ph /\ ( A =/= (/) /\ A =/= (/) ) ) )
2		pm4.24	|- ( A =/= (/) <-> ( A =/= (/) /\ A =/= (/) ) )
3	2	bicomi	|- ( ( A =/= (/) /\ A =/= (/) ) <-> A =/= (/) )
4	3	anbi2i	|- ( ( A. x e. A A. y e. A ph /\ ( A =/= (/) /\ A =/= (/) ) ) <-> ( A. x e. A A. y e. A ph /\ A =/= (/) ) )
5	1 4	bitri	|- ( AE x ( x e. A -> AE y ( y e. A -> ph ) ) <-> ( A. x e. A A. y e. A ph /\ A =/= (/) ) )