This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜓 ↔ 𝜒 )
	Assertion	mobii	⊢ ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		mobii.1	⊢ ( 𝜓 ↔ 𝜒 )
2	1	biimpri	⊢ ( 𝜒 → 𝜓 )
3	2	moimi	⊢ ( ∃* 𝑥 𝜓 → ∃* 𝑥 𝜒 )
4	1	biimpi	⊢ ( 𝜓 → 𝜒 )
5	4	moimi	⊢ ( ∃* 𝑥 𝜒 → ∃* 𝑥 𝜓 )
6	3 5	impbii	⊢ ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 𝜒 )