Theorem mobii 2548

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 2545	. 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒)
4	1	biimpi 216	. . 3 ⊢ (𝜓 → 𝜒)
5	4	moimi 2545	. 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓)
6	3, 5	impbii 209	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 206  ∃*wmo 2538

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 2540

This theorem is referenced by:  eubii  2585  cbvmo  2604  moanmo  2622  2moswapv  2629  2moswap  2644  nulmo  2713  rmobiia  3370  rmoanidOLD  3376  rmov  3495  euxfr2w  3708  euxfr2  3710  rmoan  3727  reuxfrd  3736  2reu5lem2  3744  2rmoswap  3749  dffun9  6570  funopab  6576  funcnv2  6609  funcnv  6610  fun2cnv  6612  fncnv  6614  imadif  6625  fnres  6670  ov3  7575  oprabex3  7981  brdom6disj  10551  grothprim  10853  axaddf  11164  axmulf  11165  reuxfrdf  32477  rmoun  32480  funcnvmpt  32650  rmoeqi  36210  rmoeqbii  36211  nrmo  36433  alrmomorn  38381  cosscnvssid4  38500  dfeldisj4  38743  disjres  38767  tfsconcatlem  43327  euabsneu  47024  rmotru  48749  oppcthin  49291  indthinc  49315  prsthinc  49317