Theorem mobii 2547

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

Syntax hints:   ↔ wb 206  ∃*wmo 2537

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

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-mo 2539

This theorem is referenced by:  eubii  2584  cbvmo  2603  moanmo  2621  2moswapv  2628  2moswap  2643  nulmo  2712  rmobiia  3385  rmoanidOLD  3391  rmov  3510  euxfr2w  3725  euxfr2  3727  rmoan  3744  reuxfrd  3753  2reu5lem2  3761  2rmoswap  3766  dffun9  6594  funopab  6600  funcnv2  6633  funcnv  6634  fun2cnv  6636  fncnv  6638  imadif  6649  fnres  6694  ov3  7597  oprabex3  8003  brdom6disj  10573  grothprim  10875  axaddf  11186  axmulf  11187  reuxfrdf  32511  rmoun  32514  funcnvmpt  32678  rmoeqi  36189  rmoeqbii  36190  nrmo  36412  alrmomorn  38360  cosscnvssid4  38479  dfeldisj4  38722  disjres  38746  tfsconcatlem  43354  euabsneu  47045  rmotru  48728  oppcthin  49112  indthinc  49134  prsthinc  49136