Theorem mobii 2545

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

Syntax hints:   ↔ wb 206  ∃*wmo 2535

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 2537

This theorem is referenced by:  eubii  2582  cbvmo  2601  moanmo  2619  2moswapv  2626  2moswap  2641  nulmo  2710  rmobiia  3354  rmov  3468  euxfr2w  3676  euxfr2  3678  rmoan  3695  reuxfrd  3704  2reu5lem2  3712  2rmoswap  3717  dffun9  6518  funopab  6524  funcnv2  6557  funcnv  6558  fun2cnv  6560  fncnv  6562  imadif  6573  fnres  6616  ov3  7518  oprabex3  7918  brdom6disj  10433  grothprim  10735  axaddf  11046  axmulf  11047  reuxfrdf  32481  rmoun  32484  funcnvmpt  32660  rmoeqi  36242  rmoeqbii  36243  nrmo  36465  alrmomorn  38400  cosscnvssid4  38589  dfeldisj4  38828  disjres  38852  tfsconcatlem  43443  sinnpoly  47005  euabsneu  47142  rmotru  48917  oppcthin  49553  indthinc  49577  prsthinc  49579