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  3717  euxfr2  3719  rmoan  3736  reuxfrd  3745  2reu5lem2  3753  2rmoswap  3758  dffun9  6578  funopab  6584  funcnv2  6617  funcnv  6618  fun2cnv  6620  fncnv  6622  imadif  6633  fnres  6678  ov3  7570  oprabex3  7964  brdom6disj  10527  grothprim  10829  axaddf  11140  axmulf  11141  reuxfrdf  31731  rmoun  31734  funcnvmpt  31892  nrmo  35295  alrmomorn  37227  cosscnvssid4  37347  dfeldisj4  37590  disjres  37614  tfsconcatlem  42086  euabsneu  45738  rmotru  47489  oppcthin  47659  indthinc  47672  prsthinc  47674