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

Hypothesis

Ref	Expression
mobii.1	⊢ (𝜓 ↔ 𝜒)

Assertion

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

Proof of Theorem mobii

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

Syntax hints:   ↔ wb 206  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540

This theorem is referenced by:  cbvmo  2605  moanmo  2623  2moswapv  2630  2moswap  2645  nulmo  2714  rmobiia  3349  rmov  3460  euxfr2w  3667  euxfr2  3669  rmoan  3686  reuxfrd  3695  2reu5lem2  3703  2rmoswap  3708  dffun9  6522  funopab  6528  funcnv2  6561  funcnv  6562  fun2cnv  6564  fncnv  6566  imadif  6577  fnres  6620  funcnvmpt  6944  ov3  7524  oprabex3  7924  brdom6disj  10448  grothprim  10751  axaddf  11062  axmulf  11063  reuxfrdf  32578  rmoun  32581  rmoeqi  36388  rmoeqbii  36389  nrmo  36611  alrmomorn  38696  ralmo  38698  cosscnvssid4  38905  dfeldisj4  39150  disjres  39182  tfsconcatlem  43785  sinnpoly  47354  euabsneu  47491  rmotru  49293  oppcthin  49928  indthinc  49952  prsthinc  49954