Theorem mobii 2548

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

Syntax hints:   ↔ wb 206  ∃*wmo 2537

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 2539

This theorem is referenced by:  cbvmo  2604  moanmo  2622  2moswapv  2629  2moswap  2644  nulmo  2713  rmobiia  3356  rmov  3470  euxfr2w  3678  euxfr2  3680  rmoan  3697  reuxfrd  3706  2reu5lem2  3714  2rmoswap  3719  dffun9  6521  funopab  6527  funcnv2  6560  funcnv  6561  fun2cnv  6563  fncnv  6565  imadif  6576  fnres  6619  ov3  7521  oprabex3  7921  brdom6disj  10442  grothprim  10745  axaddf  11056  axmulf  11057  reuxfrdf  32565  rmoun  32568  funcnvmpt  32745  rmoeqi  36381  rmoeqbii  36382  nrmo  36604  alrmomorn  38551  cosscnvssid4  38740  dfeldisj4  38979  disjres  39003  tfsconcatlem  43578  sinnpoly  47137  euabsneu  47274  rmotru  49048  oppcthin  49683  indthinc  49707  prsthinc  49709