Theorem mobii 2578

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

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

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 2569

This theorem is used by:  cbvmo  2634  moanmo  2652  2moswapv  2659  2moswap  2674  nulmo  2742  rmobiia  3377  rmov  3486  euxfr2w  3685  euxfr2  3687  rmoan  3704  reuxfrd  3713  2reu5lem2  3721  2rmoswap  3726  dffun9  6569  funopab  6575  funcnv2  6608  funcnv  6609  fun2cnv  6611  fncnv  6613  imadif  6624  fnres  6666  funcnvmpt  6995  ov3  7582  oprabex3  7980  brdom6disj  10531  grothprim  10834  axaddf  11145  axmulf  11146  reuxfrdf  32908  rmoun  32911  rmoeqi  36756  rmoeqbii  36757  nrmo  36978  alrmomorn  39065  ralmo  39067  cosscnvssid4  39274  dfeldisj4  39519  disjres  39551  tfsconcatlem  44121  sinnpoly  47686  euabsneu  47823  rmotru  49638  oppcthin  50273  indthinc  50297  prsthinc  50299