Theorem rmob2

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	⊢ ( 𝜑 → 𝜓 )
Assertion	rmob2	⊢ ( 𝜑 → ( 𝑥 = 𝐵 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rmoi2.1	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
2		rmoi2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		rmoi2.3	⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 )
4		rmoi2.4	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
5		rmoi2.5	⊢ ( 𝜑 → 𝜓 )
6		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜓 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
7	3 6	sylib	⊢ ( 𝜑 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
8		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
9	8 1	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
10	9	mob2	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝑥 = 𝐵 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
11	2 7 4 5 10	syl112anc	⊢ ( 𝜑 → ( 𝑥 = 𝐵 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
12	2 11	mpbirand	⊢ ( 𝜑 → ( 𝑥 = 𝐵 ↔ 𝜒 ) )