Theorem mobii 2551

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

Syntax hints:   ↔ wb 206  ∃*wmo 2541

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

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-mo 2543

This theorem is referenced by:  eubii  2588  cbvmo  2607  moanmo  2625  2moswapv  2632  2moswap  2647  nulmo  2716  rmobiia  3394  rmoanidOLD  3400  rmov  3519  euxfr2w  3742  euxfr2  3744  rmoan  3761  reuxfrd  3770  2reu5lem2  3778  2rmoswap  3783  dffun9  6607  funopab  6613  funcnv2  6646  funcnv  6647  fun2cnv  6649  fncnv  6651  imadif  6662  fnres  6707  ov3  7613  oprabex3  8018  brdom6disj  10601  grothprim  10903  axaddf  11214  axmulf  11215  reuxfrdf  32519  rmoun  32522  funcnvmpt  32685  rmoeqi  36151  rmoeqbii  36152  nrmo  36376  alrmomorn  38314  cosscnvssid4  38433  dfeldisj4  38676  disjres  38700  tfsconcatlem  43298  euabsneu  46943  rmotru  48536  oppcthin  48706  indthinc  48719  prsthinc  48721