Theorem mobii 2552

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

Syntax hints:   ↔ wb 207  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543

This theorem is referenced by:  cbvmo  2608  moanmo  2626  2moswapv  2633  2moswap  2648  nulmo  2716  rmobiia  3350  rmov  3460  euxfr2w  3661  euxfr2  3663  rmoan  3680  reuxfrd  3689  2reu5lem2  3697  2rmoswap  3702  dffun9  6514  funopab  6520  funcnv2  6553  funcnv  6554  fun2cnv  6556  fncnv  6558  imadif  6569  fnres  6612  funcnvmpt  6937  ov3  7519  oprabex3  7919  brdom6disj  10445  grothprim  10748  axaddf  11059  axmulf  11060  reuxfrdf  32578  rmoun  32581  rmoeqi  36415  rmoeqbii  36416  nrmo  36638  alrmomorn  38725  ralmo  38727  cosscnvssid4  38934  dfeldisj4  39179  disjres  39211  tfsconcatlem  43781  sinnpoly  47354  euabsneu  47491  rmotru  49293  oppcthin  49928  indthinc  49952  prsthinc  49954