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 1827	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 209  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567

This theorem is referenced by:  cbvmo  2632  moanmo  2650  2moswapv  2657  2moswap  2672  nulmo  2740  rmobiia  3375  rmov  3484  euxfr2w  3683  euxfr2  3685  rmoan  3702  reuxfrd  3711  2reu5lem2  3719  2rmoswap  3724  dffun9  6565  funopab  6571  funcnv2  6604  funcnv  6605  fun2cnv  6607  fncnv  6609  imadif  6620  fnres  6662  funcnvmpt  6991  ov3  7573  oprabex3  7970  brdom6disj  10511  grothprim  10814  axaddf  11125  axmulf  11126  reuxfrdf  32837  rmoun  32840  rmoeqi  36699  rmoeqbii  36700  nrmo  36921  alrmomorn  39007  ralmo  39009  cosscnvssid4  39216  dfeldisj4  39461  disjres  39493  tfsconcatlem  44063  sinnpoly  47628  euabsneu  47765  rmotru  49581  oppcthin  50216  indthinc  50240  prsthinc  50242