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

Syntax hints:   ↔ wb 209  ∃*wmo 2537

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

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-mo 2539

This theorem is referenced by:  eubii  2584  cbvmowOLD  2603  cbvmo  2604  moanmo  2623  2moswapv  2630  2moswap  2645  nulmo  2713  rmoanid  3237  rmobiia  3297  rmov  3425  euxfr2w  3622  euxfr2  3624  rmoan  3641  reuxfrd  3650  2reu5lem2  3658  2rmoswap  3663  dffun9  6387  funopab  6393  funcnv2  6426  funcnv  6427  fun2cnv  6429  fncnv  6431  imadif  6442  fnres  6482  ov3  7349  oprabex3  7728  brdom6disj  10111  grothprim  10413  axaddf  10724  axmulf  10725  reuxfrdf  30512  rmoun  30515  funcnvmpt  30678  nrmo  34285  alrmomorn  36176  cosscnvssid4  36281  dfeldisj4  36517  euabsneu  44137  rmotru  45766  oppcthin  45936  indthinc  45949  prsthinc  45951