Theorem mobii 2541

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

Syntax hints:   ↔ wb 206  ∃*wmo 2531

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 207  df-ex 1780  df-mo 2533

This theorem is referenced by:  eubii  2578  cbvmo  2597  moanmo  2615  2moswapv  2622  2moswap  2637  nulmo  2706  rmobiia  3357  rmoanidOLD  3363  rmov  3474  euxfr2w  3688  euxfr2  3690  rmoan  3707  reuxfrd  3716  2reu5lem2  3724  2rmoswap  3729  dffun9  6529  funopab  6535  funcnv2  6568  funcnv  6569  fun2cnv  6571  fncnv  6573  imadif  6584  fnres  6627  ov3  7532  oprabex3  7935  brdom6disj  10461  grothprim  10763  axaddf  11074  axmulf  11075  reuxfrdf  32393  rmoun  32396  funcnvmpt  32564  rmoeqi  36148  rmoeqbii  36149  nrmo  36371  alrmomorn  38313  cosscnvssid4  38441  dfeldisj4  38685  disjres  38709  tfsconcatlem  43298  sinnpoly  46865  euabsneu  47002  rmotru  48764  oppcthin  49400  indthinc  49424  prsthinc  49426