Theorem mobii 2579

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

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

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 2570

This theorem is used by:  cbvmo  2635  moanmo  2653  2moswapv  2660  2moswap  2675  nulmo  2743  rmobiia  3378  rmov  3487  euxfr2w  3686  euxfr2  3688  rmoan  3705  reuxfrd  3714  2reu5lem2  3722  2rmoswap  3727  dffun9  6569  funopab  6575  funcnv2  6608  funcnv  6609  fun2cnv  6611  fncnv  6613  imadif  6624  fnres  6666  funcnvmpt  6995  ov3  7579  oprabex3  7976  brdom6disj  10526  grothprim  10829  axaddf  11140  axmulf  11141  reuxfrdf  32852  rmoun  32855  rmoeqi  36731  rmoeqbii  36732  nrmo  36953  alrmomorn  39039  ralmo  39041  cosscnvssid4  39248  dfeldisj4  39493  disjres  39525  tfsconcatlem  44095  sinnpoly  47660  euabsneu  47797  rmotru  49613  oppcthin  50248  indthinc  50272  prsthinc  50274