Theorem mobii 2543

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

Syntax hints:   ↔ wb 206  ∃*wmo 2533

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-mo 2535

This theorem is referenced by:  eubii  2580  cbvmo  2599  moanmo  2617  2moswapv  2624  2moswap  2639  nulmo  2708  rmobiia  3352  rmov  3466  euxfr2w  3674  euxfr2  3676  rmoan  3693  reuxfrd  3702  2reu5lem2  3710  2rmoswap  3715  dffun9  6510  funopab  6516  funcnv2  6549  funcnv  6550  fun2cnv  6552  fncnv  6554  imadif  6565  fnres  6608  ov3  7509  oprabex3  7909  brdom6disj  10423  grothprim  10725  axaddf  11036  axmulf  11037  reuxfrdf  32470  rmoun  32473  funcnvmpt  32649  rmoeqi  36229  rmoeqbii  36230  nrmo  36452  alrmomorn  38394  cosscnvssid4  38522  dfeldisj4  38766  disjres  38790  tfsconcatlem  43377  sinnpoly  46930  euabsneu  47067  rmotru  48842  oppcthin  49478  indthinc  49502  prsthinc  49504