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

Syntax hints:   ↔ wb 205  ∃*wmo 2533

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-mo 2535

This theorem is referenced by:  eubii  2580  cbvmowOLD  2599  cbvmo  2600  moanmo  2619  2moswapv  2626  2moswap  2641  nulmo  2709  rmobiia  3383  rmoanidOLD  3389  rmov  3502  euxfr2w  3714  euxfr2  3716  rmoan  3733  reuxfrd  3742  2reu5lem2  3750  2rmoswap  3755  dffun9  6569  funopab  6575  funcnv2  6608  funcnv  6609  fun2cnv  6611  fncnv  6613  imadif  6624  fnres  6667  ov3  7557  oprabex3  7951  brdom6disj  10514  grothprim  10816  axaddf  11127  axmulf  11128  reuxfrdf  31696  rmoun  31699  funcnvmpt  31861  nrmo  35200  alrmomorn  37133  cosscnvssid4  37253  dfeldisj4  37496  disjres  37520  tfsconcatlem  41957  euabsneu  45611  rmotru  47329  oppcthin  47499  indthinc  47512  prsthinc  47514