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

Theorem mobii 2641
Description: Formula-building rule for "at most one" quantifier (inference rule). (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
StepHypRef Expression
1 mobii.1 . . . 4 (𝜓𝜒)
21a1i 11 . . 3 (⊤ → (𝜓𝜒))
32mobidv 2639 . 2 (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
43trud 1641 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wtru 1632  ∃*wmo 2619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-tru 1634  df-ex 1853  df-nf 1858  df-eu 2622  df-mo 2623
This theorem is referenced by:  moanmo  2681  2moswap  2696  rmobiia  3281  rmov  3374  euxfr2  3543  rmoan  3558  2reu5lem2  3566  reuxfr2d  5019  dffun9  6060  funopab  6066  funcnv2  6097  funcnv  6098  fun2cnv  6100  fncnv  6102  imadif  6113  fnres  6147  ov3  6944  oprabex3  7304  brdom6disj  9556  grothprim  9858  axaddf  10168  axmulf  10169  reuxfr3d  29668  funcnvmptOLD  29807  funcnvmpt  29808  alrmomorn  34465  cosscnvssid4  34569  2rmoswap  41704
  Copyright terms: Public domain W3C validator