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 1829	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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

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

This theorem is used by:  cbvmo  2629  moanmo  2647  2moswapv  2654  2moswap  2669  nulmo  2737  rmobiia  3371  rmov  3479  euxfr2w  3677  euxfr2  3679  rmoan  3696  reuxfrd  3705  2reu5lem2  3713  2rmoswap  3718  dffun9  6574  funopab  6580  funcnv2  6613  funcnv  6614  fun2cnv  6616  fncnv  6618  imadif  6629  fnres  6671  funcnvmpt  7000  ov3  7587  funmpt3  7691  mpt3fvd  7692  oprabex3  7993  brdom6disj  10618  grothprim  10926  axaddf  11237  axmulf  11238  reuxfrdf  33138  rmoun  33141  rmoeqi  37100  rmoeqbii  37101  nrmo  37322  alrmomorn  39427  ralmo  39429  cosscnvssid4  39636  dfeldisj4  39881  disjres  39913  tfsconcatlem  44475  sinnpoly  48077  euabsneu  48234  rmotru  50049  oppcthin  50709  indthinc  50733  prsthinc  50735