Theorem mobii 2542

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 1913. (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 227	. . 3 ⊢ (𝜒 → 𝜓)
3	2	moimi 2539	. 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒)
4	1	biimpi 215	. . 3 ⊢ (𝜓 → 𝜒)
5	4	moimi 2539	. 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓)
6	3, 5	impbii 208	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 205  ∃*wmo 2532

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

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-mo 2534

This theorem is referenced by:  eubii  2579  cbvmowOLD  2598  cbvmo  2599  moanmo  2618  2moswapv  2625  2moswap  2640  nulmo  2708  rmobiia  3382  rmoanidOLD  3388  rmov  3501  euxfr2w  3716  euxfr2  3718  rmoan  3735  reuxfrd  3744  2reu5lem2  3752  2rmoswap  3757  dffun9  6577  funopab  6583  funcnv2  6616  funcnv  6617  fun2cnv  6619  fncnv  6621  imadif  6632  fnres  6677  ov3  7569  oprabex3  7963  brdom6disj  10526  grothprim  10828  axaddf  11139  axmulf  11140  reuxfrdf  31726  rmoun  31729  funcnvmpt  31887  nrmo  35290  alrmomorn  37222  cosscnvssid4  37342  dfeldisj4  37585  disjres  37609  tfsconcatlem  42076  euabsneu  45728  rmotru  47479  oppcthin  47649  indthinc  47662  prsthinc  47664