Theorem rmoi2

Description: Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019)

	Ref	Expression
Hypotheses	rmoi2.1	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	rmoi2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	rmoi2.3	⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 )
	rmoi2.4	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
	rmoi2.5	⊢ ( 𝜑 → 𝜓 )
	rmoi2.6	⊢ ( 𝜑 → 𝜒 )
Assertion	rmoi2	⊢ ( 𝜑 → 𝑥 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rmoi2.1	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
2		rmoi2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		rmoi2.3	⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 )
4		rmoi2.4	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
5		rmoi2.5	⊢ ( 𝜑 → 𝜓 )
6		rmoi2.6	⊢ ( 𝜑 → 𝜒 )
7	1 2 3 4 5	rmob2	⊢ ( 𝜑 → ( 𝑥 = 𝐵 ↔ 𝜒 ) )
8	6 7	mpbird	⊢ ( 𝜑 → 𝑥 = 𝐵 )