Theorem ralsanmo

Description: An "all some" statement restricted to a class, conjoined with the claim that at most one x in A satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one x in A satisfies the antecedent. This is the restricted counterpart of alsanmo . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	ralsanmo	|- ( ( AE x e. A ( ph -> ps ) /\ E* x e. A ph ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-rals	|- ( AE x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
2	1	anbi1i	|- ( ( AE x e. A ( ph -> ps ) /\ E* x e. A ph ) <-> ( ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) /\ E* x e. A ph ) )
3		anass	|- ( ( ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) /\ E* x e. A ph ) <-> ( A. x e. A ( ph -> ps ) /\ ( E. x e. A ph /\ E* x e. A ph ) ) )
4		reu5	|- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
5	4	bicomi	|- ( ( E. x e. A ph /\ E* x e. A ph ) <-> E! x e. A ph )
6	5	anbi2i	|- ( ( A. x e. A ( ph -> ps ) /\ ( E. x e. A ph /\ E* x e. A ph ) ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
7	2 3 6	3bitri	|- ( ( AE x e. A ( ph -> ps ) /\ E* x e. A ph ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )