Theorem mobii 2546

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

Syntax hints:   ↔ wb 205  ∃*wmo 2536

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 206  df-ex 1780  df-mo 2538

This theorem is referenced by:  eubii  2583  cbvmowOLD  2602  cbvmo  2603  moanmo  2622  2moswapv  2629  2moswap  2644  nulmo  2712  rmoanid  3311  rmobiia  3342  rmov  3464  euxfr2w  3660  euxfr2  3662  rmoan  3679  reuxfrd  3688  2reu5lem2  3696  2rmoswap  3701  dffun9  6492  funopab  6498  funcnv2  6531  funcnv  6532  fun2cnv  6534  fncnv  6536  imadif  6547  fnres  6590  ov3  7467  oprabex3  7852  brdom6disj  10334  grothprim  10636  axaddf  10947  axmulf  10948  reuxfrdf  30884  rmoun  30887  funcnvmpt  31049  nrmo  34644  alrmomorn  36532  cosscnvssid4  36637  dfeldisj4  36873  euabsneu  44580  rmotru  46208  oppcthin  46378  indthinc  46391  prsthinc  46393