Metamath Proof Explorer


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 ( 𝜑 → ( 𝑥 = 𝐵𝜒 ) )