Theorem mobii 2582

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.)

Hypothesis

Ref	Expression
mobii.1	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
mobii	⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		mobi 2581	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
2		mobii.1	. 2 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	mpg 1824	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 209  ∃*wmo 2571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573

This theorem is referenced by:  cbvmo  2638  moanmo  2656  2moswapv  2663  2moswap  2678  nulmo  2746  rmobiia  3382  rmov  3492  euxfr2w  3692  euxfr2  3694  rmoan  3711  reuxfrd  3720  2reu5lem2  3728  2rmoswap  3733  dffun9  6566  funopab  6572  funcnv2  6605  funcnv  6606  fun2cnv  6608  fncnv  6610  imadif  6621  fnres  6663  funcnvmpt  6992  ov3  7574  oprabex3  7973  brdom6disj  10515  grothprim  10818  axaddf  11129  axmulf  11130  reuxfrdf  32777  rmoun  32780  rmoeqi  36587  rmoeqbii  36588  nrmo  36809  alrmomorn  38896  ralmo  38898  cosscnvssid4  39105  dfeldisj4  39350  disjres  39382  tfsconcatlem  43954  sinnpoly  47516  euabsneu  47653  rmotru  49465  oppcthin  50100  indthinc  50124  prsthinc  50126