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

Syntax hints:   ↔ wb 206  ∃*wmo 2536

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

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-mo 2538

This theorem is referenced by:  eubii  2583  cbvmo  2602  moanmo  2620  2moswapv  2627  2moswap  2642  nulmo  2711  rmobiia  3384  rmoanidOLD  3390  rmov  3509  euxfr2w  3729  euxfr2  3731  rmoan  3748  reuxfrd  3757  2reu5lem2  3765  2rmoswap  3770  dffun9  6597  funopab  6603  funcnv2  6636  funcnv  6637  fun2cnv  6639  fncnv  6641  imadif  6652  fnres  6696  ov3  7596  oprabex3  8001  brdom6disj  10570  grothprim  10872  axaddf  11183  axmulf  11184  reuxfrdf  32519  rmoun  32522  funcnvmpt  32684  rmoeqi  36169  rmoeqbii  36170  nrmo  36393  alrmomorn  38340  cosscnvssid4  38459  dfeldisj4  38702  disjres  38726  tfsconcatlem  43326  euabsneu  46978  rmotru  48652  oppcthin  48839  indthinc  48853  prsthinc  48855