Theorem mobii 2548

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 2547	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
2		mobii.1	. 2 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	mpg 1799	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 206  ∃*wmo 2537

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 2539

This theorem is referenced by:  cbvmo  2604  moanmo  2622  2moswapv  2629  2moswap  2644  nulmo  2713  rmobiia  3348  rmov  3459  euxfr2w  3666  euxfr2  3668  rmoan  3685  reuxfrd  3694  2reu5lem2  3702  2rmoswap  3707  dffun9  6527  funopab  6533  funcnv2  6566  funcnv  6567  fun2cnv  6569  fncnv  6571  imadif  6582  fnres  6625  funcnvmpt  6949  ov3  7530  oprabex3  7930  brdom6disj  10454  grothprim  10757  axaddf  11068  axmulf  11069  reuxfrdf  32560  rmoun  32563  rmoeqi  36369  rmoeqbii  36370  nrmo  36592  alrmomorn  38679  ralmo  38681  cosscnvssid4  38888  dfeldisj4  39133  disjres  39165  tfsconcatlem  43764  sinnpoly  47339  euabsneu  47476  rmotru  49278  oppcthin  49913  indthinc  49937  prsthinc  49939