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  3358  rmov  3472  euxfr2w  3680  euxfr2  3682  rmoan  3699  reuxfrd  3708  2reu5lem2  3716  2rmoswap  3721  dffun9  6529  funopab  6535  funcnv2  6568  funcnv  6569  fun2cnv  6571  fncnv  6573  imadif  6584  fnres  6627  funcnvmpt  6951  ov3  7531  oprabex3  7931  brdom6disj  10454  grothprim  10757  axaddf  11068  axmulf  11069  reuxfrdf  32577  rmoun  32580  rmoeqi  36403  rmoeqbii  36404  nrmo  36626  alrmomorn  38609  ralmo  38611  cosscnvssid4  38818  dfeldisj4  39063  disjres  39095  tfsconcatlem  43693  sinnpoly  47251  euabsneu  47388  rmotru  49162  oppcthin  49797  indthinc  49821  prsthinc  49823