Theorem mobii 2574

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

This proof depends on syntax axioms:   ↔ wb 209  ∃*wmo 2563

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565

This theorem is used by:  cbvmo  2630  moanmo  2648  2moswapv  2655  2moswap  2670  nulmo  2738  rmobiia  3372  rmov  3480  euxfr2w  3678  euxfr2  3680  rmoan  3697  reuxfrd  3706  2reu5lem2  3714  2rmoswap  3719  dffun9  6569  funopab  6575  funcnv2  6608  funcnv  6609  fun2cnv  6611  fncnv  6613  imadif  6624  fnres  6666  funcnvmpt  6995  ov3  7583  funmpt3  7687  mpt3fvd  7688  oprabex3  7989  brdom6disj  10611  grothprim  10919  axaddf  11230  axmulf  11231  reuxfrdf  33087  rmoun  33090  rmoeqi  36976  rmoeqbii  36977  nrmo  37198  alrmomorn  39290  ralmo  39292  cosscnvssid4  39499  dfeldisj4  39744  disjres  39776  tfsconcatlem  44337  sinnpoly  47940  euabsneu  48097  rmotru  49912  oppcthin  50545  indthinc  50569  prsthinc  50571