Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mobii GIF version

Theorem mobii 2012
 Description: Formula-building rule for "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
StepHypRef Expression
1 mobii.1 . . . 4 (𝜓𝜒)
21a1i 9 . . 3 (⊤ → (𝜓𝜒))
32mobidv 2011 . 2 (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
43mptru 1323 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104  ⊤wtru 1315  ∃*wmo 1976 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497 This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-eu 1978  df-mo 1979 This theorem is referenced by:  moaneu  2051  moanmo  2052  2moswapdc  2065  2exeu  2067  rmobiia  2595  rmov  2678  euxfr2dc  2840  rmoan  2855  2rmorex  2861  mosn  3528  dffun9  5120  funopab  5126  funco  5131  funcnv2  5151  funcnv  5152  fun2cnv  5155  fncnv  5157  imadif  5171  fnres  5207  ovi3  5873  oprabex3  5993  axaddf  7640  axmulf  7641  frecuzrdgtcl  10125  frecuzrdgfunlem  10132  fsum3  11096
 Copyright terms: Public domain W3C validator