MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mobii Structured version   Visualization version   GIF version

Theorem mobii 2606
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.) Avoid ax-5 1911. (Revised by Wolf Lammen, 24-Sep-2023.)
Hypothesis
Ref Expression
mobii.1 (𝜓𝜒)
Assertion
Ref Expression
mobii (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Proof of Theorem mobii
StepHypRef Expression
1 mobii.1 . . . 4 (𝜓𝜒)
21biimpri 231 . . 3 (𝜒𝜓)
32moimi 2603 . 2 (∃*𝑥𝜓 → ∃*𝑥𝜒)
41biimpi 219 . . 3 (𝜓𝜒)
54moimi 2603 . 2 (∃*𝑥𝜒 → ∃*𝑥𝜓)
63, 5impbii 212 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 209  ∃*wmo 2596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-mo 2598
This theorem is referenced by:  eubii  2645  cbvmowOLD  2664  cbvmo  2665  moanmo  2684  2moswapv  2691  2moswap  2706  nulmo  2775  rmoanid  3287  rmobiia  3348  rmov  3469  euxfr2w  3659  euxfr2  3661  rmoan  3678  reuxfrd  3687  2reu5lem2  3695  2rmoswap  3700  dffun9  6353  funopab  6359  funcnv2  6392  funcnv  6393  fun2cnv  6395  fncnv  6397  imadif  6408  fnres  6446  ov3  7291  oprabex3  7660  brdom6disj  9943  grothprim  10245  axaddf  10556  axmulf  10557  reuxfrdf  30262  rmoun  30265  funcnvmpt  30430  nrmo  33868  alrmomorn  35769  cosscnvssid4  35874  dfeldisj4  36110  euabsneu  43615
  Copyright terms: Public domain W3C validator