Theorem mobii

Description: Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 17-Oct-2016) Avoid ax-5 . (Revised by Wolf Lammen, 24-Sep-2023)

	Ref	Expression
Hypothesis	mobii.1	$$⊢\psi \leftrightarrow \chi$$
Assertion	mobii	$$⊢{\exists }^{*}x\psi \leftrightarrow {\exists }^{*}x\chi$$

Proof

Step	Hyp	Ref	Expression
1		mobii.1	$$⊢\psi \leftrightarrow \chi$$
2	1	biimpri	$$⊢\chi \to \psi$$
3	2	moimi	$$⊢{\exists }^{*}x\psi \to {\exists }^{*}x\chi$$
4	1	biimpi	$$⊢\psi \to \chi$$
5	4	moimi	$$⊢{\exists }^{*}x\chi \to {\exists }^{*}x\psi$$
6	3 5	impbii	$$⊢{\exists }^{*}x\psi \leftrightarrow {\exists }^{*}x\chi$$