Theorem mobii 2588

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 1892. (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 229	. . 3 ⊢ (𝜒 → 𝜓)
3	2	moimi 2583	. 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒)
4	1	biimpi 217	. . 3 ⊢ (𝜓 → 𝜒)
5	4	moimi 2583	. 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓)
6	3, 5	impbii 210	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 207  ∃*wmo 2576

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

This theorem depends on definitions:  df-bi 208  df-ex 1766  df-mo 2578

This theorem is referenced by:  eubii  2632  cbvmo  2656  moanmo  2678  2moswapv  2686  2moswap  2701  nulmo  2776  rmoanid  3292  rmobiia  3357  rmov  3468  euxfr2  3652  rmoan  3669  reuxfrd  3678  2reu5lem2  3686  2rmoswap  3691  dffun9  6261  funopab  6267  funcnv2  6299  funcnv  6300  fun2cnv  6302  fncnv  6304  imadif  6315  fnres  6351  ov3  7174  oprabex3  7541  brdom6disj  9807  grothprim  10109  axaddf  10420  axmulf  10421  reuxfrdf  29943  rmoun  29946  funcnvmpt  30098  nrmo  33369  alrmomorn  35165  cosscnvssid4  35269  dfeldisj4  35505  euabsneu  42801