Metamath Proof Explorer

Theorem mob

Description: Equality implied by "at most one". (Contributed by NM, 18-Feb-2006)

Ref Expression
Hypotheses moi.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
moi.2 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion mob ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 moi.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 moi.2 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
3 elex ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V )
4 nfv ⊢ Ⅎ 𝑥 𝐵 ∈ V
5 nfmo1 ⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
6 nfv ⊢ Ⅎ 𝑥 𝜓
7 4 5 6 nf3an ⊢ Ⅎ 𝑥 ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜓 )
8 nfv ⊢ Ⅎ 𝑥 ( 𝐴 = 𝐵 ↔ 𝜒 )
9 7 8 nfim ⊢ Ⅎ 𝑥 ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) )
10 1 3anbi3d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) ↔ ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) ) )
11 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) )
12 11 bibi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐵 ↔ 𝜒 ) ↔ ( 𝐴 = 𝐵 ↔ 𝜒 ) ) )
13 10 12 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝑥 = 𝐵 ↔ 𝜒 ) ) ↔ ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) ) )
14 2 mob2 ⊢ ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝑥 = 𝐵 ↔ 𝜒 ) )
15 9 13 14 vtoclg1f ⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) )
16 15 com12 ⊢ ( ( 𝐵 ∈ V ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 ∈ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) )
17 16 3expib ⊢ ( 𝐵 ∈ V → ( ( ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 ∈ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) ) )
18 3 17 syl ⊢ ( 𝐵 ∈ 𝐷 → ( ( ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 ∈ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) ) )
19 18 com3r ⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( ( ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) ) )
20 19 imp ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) ) )
21 20 3impib ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) )