# Metamath Proof Explorer

## Theorem mob

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

Ref Expression
Hypotheses moi.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
moi.2 ${⊢}{x}={B}\to \left({\phi }↔{\chi }\right)$
Assertion mob ${⊢}\left(\left({A}\in {C}\wedge {B}\in {D}\right)\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 moi.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
2 moi.2 ${⊢}{x}={B}\to \left({\phi }↔{\chi }\right)$
3 elex ${⊢}{B}\in {D}\to {B}\in \mathrm{V}$
4 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{V}$
5 nfmo1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
6 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
7 4 5 6 nf3an ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)$
8 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}={B}↔{\chi }\right)$
9 7 8 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)\right)$
10 1 3anbi3d ${⊢}{x}={A}\to \left(\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\phi }\right)↔\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\right)$
11 eqeq1 ${⊢}{x}={A}\to \left({x}={B}↔{A}={B}\right)$
12 11 bibi1d ${⊢}{x}={A}\to \left(\left({x}={B}↔{\chi }\right)↔\left({A}={B}↔{\chi }\right)\right)$
13 10 12 imbi12d ${⊢}{x}={A}\to \left(\left(\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\phi }\right)\to \left({x}={B}↔{\chi }\right)\right)↔\left(\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)\right)\right)$
14 2 mob2 ${⊢}\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\phi }\right)\to \left({x}={B}↔{\chi }\right)$
15 9 13 14 vtoclg1f ${⊢}{A}\in {C}\to \left(\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)\right)$
16 15 com12 ${⊢}\left({B}\in \mathrm{V}\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}\in {C}\to \left({A}={B}↔{\chi }\right)\right)$
17 16 3expib ${⊢}{B}\in \mathrm{V}\to \left(\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}\in {C}\to \left({A}={B}↔{\chi }\right)\right)\right)$
18 3 17 syl ${⊢}{B}\in {D}\to \left(\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}\in {C}\to \left({A}={B}↔{\chi }\right)\right)\right)$
19 18 com3r ${⊢}{A}\in {C}\to \left({B}\in {D}\to \left(\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)\right)\right)$
20 19 imp ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)\right)$
21 20 3impib ${⊢}\left(\left({A}\in {C}\wedge {B}\in {D}\right)\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \left({A}={B}↔{\chi }\right)$