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

Theorem mobii 2588
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 1892. (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 229 . . 3 (𝜒𝜓)
32moimi 2583 . 2 (∃*𝑥𝜓 → ∃*𝑥𝜒)
41biimpi 217 . . 3 (𝜓𝜒)
54moimi 2583 . 2 (∃*𝑥𝜒 → ∃*𝑥𝜓)
63, 5impbii 210 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 207  ∃*wmo 2576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795
This theorem depends on definitions:  df-bi 208  df-ex 1766  df-mo 2578
This theorem is referenced by:  eubii  2632  cbvmo  2656  moanmo  2678  2moswapv  2686  2moswap  2701  nulmo  2776  rmoanid  3292  rmobiia  3357  rmov  3468  euxfr2  3652  rmoan  3669  reuxfrd  3678  2reu5lem2  3686  2rmoswap  3691  dffun9  6261  funopab  6267  funcnv2  6299  funcnv  6300  fun2cnv  6302  fncnv  6304  imadif  6315  fnres  6351  ov3  7174  oprabex3  7541  brdom6disj  9807  grothprim  10109  axaddf  10420  axmulf  10421  reuxfrdf  29943  rmoun  29946  funcnvmpt  30098  nrmo  33369  alrmomorn  35165  cosscnvssid4  35269  dfeldisj4  35505  euabsneu  42801
  Copyright terms: Public domain W3C validator