Theorem mobii 2573

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

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

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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  cbvmo  2629  moanmo  2647  2moswapv  2654  2moswap  2669  nulmo  2737  rmobiia  3371  rmov  3479  euxfr2w  3678  euxfr2  3680  rmoan  3697  reuxfrd  3706  2reu5lem2  3714  2rmoswap  3719  dffun9  6563  funopab  6569  funcnv2  6602  funcnv  6603  fun2cnv  6605  fncnv  6607  imadif  6618  fnres  6660  funcnvmpt  6989  ov3  7577  oprabex3  7975  brdom6disj  10536  grothprim  10844  axaddf  11155  axmulf  11156  reuxfrdf  32967  rmoun  32970  rmoeqi  36808  rmoeqbii  36809  nrmo  37030  alrmomorn  39107  ralmo  39109  cosscnvssid4  39316  dfeldisj4  39561  disjres  39593  tfsconcatlem  44178  sinnpoly  47760  euabsneu  47917  rmotru  49732  oppcthin  50365  indthinc  50389  prsthinc  50391