Theorem ralsanmo 50907

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

Assertion

Ref	Expression
ralsanmo	⊢ ((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))

Proof of Theorem ralsanmo

Step	Hyp	Ref	Expression
1		df-rals 50885	. . 3 ⊢ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑))
2	1	anbi1i 636	. 2 ⊢ ((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ ((∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑) ∧ ∃*𝑥 ∈ 𝐴 𝜑))
3		anass 474	. 2 ⊢ (((∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)))
4		reu5 3367	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
5	4	bicomi 227	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑)
6	5	anbi2i 635	. 2 ⊢ ((∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
7	2, 3, 6	3bitri 300	1 ⊢ ((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wral 3076  ∃wrex 3086  ∃!wreu 3363  ∃*wrmo 3364  ∀∃wrals 50883

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2594  df-rex 3087  df-rmo 3365  df-reu 3366  df-rals 50885

This theorem is used by: (None)