Theorem mobii 2575

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

Syntax hints:   ↔ wb 208  ∃*wmo 2564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-mo 2566

This theorem is referenced by:  cbvmo  2631  moanmo  2649  2moswapv  2656  2moswap  2671  nulmo  2739  rmobiia  3373  rmov  3483  euxfr2w  3683  euxfr2  3685  rmoan  3702  reuxfrd  3711  2reu5lem2  3719  2rmoswap  3724  dffun9  6550  funopab  6556  funcnv2  6589  funcnv  6590  fun2cnv  6592  fncnv  6594  imadif  6605  fnres  6648  funcnvmpt  6977  ov3  7559  oprabex3  7958  brdom6disj  10489  grothprim  10792  axaddf  11103  axmulf  11104  reuxfrdf  32687  rmoun  32690  rmoeqi  36544  rmoeqbii  36545  nrmo  36767  alrmomorn  38854  ralmo  38856  cosscnvssid4  39063  dfeldisj4  39308  disjres  39340  tfsconcatlem  43910  sinnpoly  47482  euabsneu  47619  rmotru  49421  oppcthin  50056  indthinc  50080  prsthinc  50082