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  3349  rmoanidOLD  3355  rmov  3466  euxfr2w  3680  euxfr2  3682  rmoan  3699  reuxfrd  3708  2reu5lem2  3716  2rmoswap  3721  dffun9  6511  funopab  6517  funcnv2  6550  funcnv  6551  fun2cnv  6553  fncnv  6555  imadif  6566  fnres  6609  ov3  7512  oprabex3  7912  brdom6disj  10426  grothprim  10728  axaddf  11039  axmulf  11040  reuxfrdf  32435  rmoun  32438  funcnvmpt  32610  rmoeqi  36161  rmoeqbii  36162  nrmo  36384  alrmomorn  38326  cosscnvssid4  38454  dfeldisj4  38698  disjres  38722  tfsconcatlem  43309  sinnpoly  46875  euabsneu  47012  rmotru  48787  oppcthin  49423  indthinc  49447  prsthinc  49449