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

Theorem mobii 1953
 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 9 . . 3 (⊤ → (𝜓𝜒))
32mobidv 1952 . 2 (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
43trud 1268 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
 Colors of variables: wff set class Syntax hints:   ↔ wb 102  ⊤wtru 1260  ∃*wmo 1917 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-eu 1919  df-mo 1920 This theorem is referenced by:  moaneu  1992  moanmo  1993  2moswapdc  2006  2exeu  2008  rmobiia  2516  rmov  2591  euxfr2dc  2749  rmoan  2762  2rmorex  2768  mosn  3434  dffun9  4958  funopab  4963  funco  4968  funcnv2  4987  funcnv  4988  fun2cnv  4991  fncnv  4993  imadif  5007  fnres  5043  ovi3  5665  oprabex3  5784  frecuzrdgfn  9362
 Copyright terms: Public domain W3C validator