Theorem mobii 2546

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

Syntax hints:   ↔ wb 206  ∃*wmo 2535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2537

This theorem is referenced by:  cbvmo  2602  moanmo  2620  2moswapv  2627  2moswap  2642  nulmo  2711  rmobiia  3354  rmov  3468  euxfr2w  3676  euxfr2  3678  rmoan  3695  reuxfrd  3704  2reu5lem2  3712  2rmoswap  3717  dffun9  6519  funopab  6525  funcnv2  6558  funcnv  6559  fun2cnv  6561  fncnv  6563  imadif  6574  fnres  6617  ov3  7519  oprabex3  7919  brdom6disj  10440  grothprim  10743  axaddf  11054  axmulf  11055  reuxfrdf  32514  rmoun  32517  funcnvmpt  32694  rmoeqi  36330  rmoeqbii  36331  nrmo  36553  alrmomorn  38490  cosscnvssid4  38679  dfeldisj4  38918  disjres  38942  tfsconcatlem  43520  sinnpoly  47079  euabsneu  47216  rmotru  48990  oppcthin  49625  indthinc  49649  prsthinc  49651