Theorem mobii 2576

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

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

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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  cbvmo  2632  moanmo  2650  2moswapv  2657  2moswap  2672  nulmo  2740  rmobiia  3375  rmov  3483  euxfr2w  3681  euxfr2  3683  rmoan  3700  reuxfrd  3709  2reu5lem2  3717  2rmoswap  3722  dffun9  6597  funopab  6603  funcnv2  6638  funcnv  6639  fun2cnv  6641  fncnv  6643  imadif  6654  fnres  6696  funcnvmpt  7026  ov3  7615  funmpt3  7719  mpt3fvd  7720  oprabex3  8023  brdom6disj  10650  grothprim  10958  axaddf  11269  axmulf  11270  reuxfrdf  33186  rmoun  33189  rmoeqi  37191  rmoeqbii  37192  nrmo  37413  alrmomorn  39556  ralmo  39558  cosscnvssid4  39765  dfeldisj4  40010  disjres  40042  tfsconcatlem  44599  sinnpoly  48214  euabsneu  48371  rmotru  50244  oppcthin  50904  indthinc  50928  prsthinc  50930