Theorem mobii 2549

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 1916. (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 227	. . 3 ⊢ (𝜒 → 𝜓)
3	2	moimi 2546	. 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒)
4	1	biimpi 215	. . 3 ⊢ (𝜓 → 𝜒)
5	4	moimi 2546	. 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓)
6	3, 5	impbii 208	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 205  ∃*wmo 2539

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

This theorem depends on definitions:  df-bi 206  df-ex 1786  df-mo 2541

This theorem is referenced by:  eubii  2586  cbvmowOLD  2605  cbvmo  2606  moanmo  2625  2moswapv  2632  2moswap  2647  nulmo  2715  rmoanid  3259  rmobiia  3328  rmov  3457  euxfr2w  3658  euxfr2  3660  rmoan  3677  reuxfrd  3686  2reu5lem2  3694  2rmoswap  3699  dffun9  6459  funopab  6465  funcnv2  6498  funcnv  6499  fun2cnv  6501  fncnv  6503  imadif  6514  fnres  6555  ov3  7426  oprabex3  7806  brdom6disj  10272  grothprim  10574  axaddf  10885  axmulf  10886  reuxfrdf  30818  rmoun  30821  funcnvmpt  30983  nrmo  34578  alrmomorn  36469  cosscnvssid4  36574  dfeldisj4  36810  euabsneu  44473  rmotru  46102  oppcthin  46272  indthinc  46285  prsthinc  46287