Theorem mobii 2541

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 1910. (Revised by Wolf Lammen, 24-Sep-2023.)

Hypothesis

Ref	Expression
mobii.1	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
mobii	⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Proof of Theorem mobii

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

Syntax hints:   ↔ wb 206  ∃*wmo 2531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-mo 2533

This theorem is referenced by:  eubii  2578  cbvmo  2597  moanmo  2615  2moswapv  2622  2moswap  2637  nulmo  2706  rmobiia  3360  rmoanidOLD  3366  rmov  3477  euxfr2w  3691  euxfr2  3693  rmoan  3710  reuxfrd  3719  2reu5lem2  3727  2rmoswap  3732  dffun9  6545  funopab  6551  funcnv2  6584  funcnv  6585  fun2cnv  6587  fncnv  6589  imadif  6600  fnres  6645  ov3  7552  oprabex3  7956  brdom6disj  10485  grothprim  10787  axaddf  11098  axmulf  11099  reuxfrdf  32420  rmoun  32423  funcnvmpt  32591  rmoeqi  36175  rmoeqbii  36176  nrmo  36398  alrmomorn  38340  cosscnvssid4  38468  dfeldisj4  38712  disjres  38736  tfsconcatlem  43325  euabsneu  47026  rmotru  48788  oppcthin  49424  indthinc  49448  prsthinc  49450