Metamath Proof Explorer

Theorem rmob

Description: Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypotheses rmoi.b ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
rmoi.c ⊢ ( 𝑥 = 𝐶 → ( 𝜑 ↔ 𝜒 ) )
Assertion rmob ( ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 rmoi.b ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2 rmoi.c ⊢ ( 𝑥 = 𝐶 → ( 𝜑 ↔ 𝜒 ) )
3 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
4 simprl ⊢ ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → 𝐵 ∈ 𝐴 )
5 eleq1 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
6 4 5 syl5ibcom ⊢ ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝐵 = 𝐶 → 𝐶 ∈ 𝐴 ) )
7 simpl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) → 𝐶 ∈ 𝐴 )
8 7 a1i ⊢ ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) → 𝐶 ∈ 𝐴 ) )
9 4 anim1i ⊢ ( ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) )
10 simpll ⊢ ( ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) ∧ 𝐶 ∈ 𝐴 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
11 simplr ⊢ ( ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) )
12 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
13 12 1 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) )
14 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
15 14 2 anbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) )
16 13 15 mob ⊢ ( ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) )
17 9 10 11 16 syl3anc ⊢ ( ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 = 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) )
18 17 ex ⊢ ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 = 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) ) )
19 6 8 18 pm5.21ndd ⊢ ( ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) )
20 3 19 sylanb ⊢ ( ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜒 ) ) )