MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimiv Structured version   Unicode version

Theorem exlimiv 1687
Description: Inference from Theorem 19.23 of [Margaris] p. 90, see 19.23 1841.

This inference, along with our many variants such as rexlimdv 2830, is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.appstate.edu/~hirstjl/primer/hirst.pdf. In informal proofs, the statement "Let  C be an element such that..." almost always means an implicit application of Rule C.

In essence, Rule C states that if we can prove that some element  x exists satisfying a wff, i.e.  E. x ph ( x ) where  ph ( x ) has  x free, then we can use  ph ( C ) as a hypothesis for the proof where  C is a new (fictitious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier.

We cannot do this in Metamath directly. Instead, we use the original  ph (containing  x) as an antecedent for the main part of the proof. We eventually arrive at  ( ph  ->  ps ) where  ps is the theorem to be proved and does not contain  x. Then we apply exlimiv 1687 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 5 to arrive at the final theorem  ps. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-6 and ax-8, 4-Dec-2017.)

Hypothesis
Ref Expression
exlimiv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimiv  |-  ( E. x ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem exlimiv
StepHypRef Expression
1 exlimiv.1 . . 3  |-  ( ph  ->  ps )
21eximi 1626 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax5e 1671 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 16 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669
This theorem depends on definitions:  df-bi 185  df-ex 1590
This theorem is referenced by:  exlimivv  1688  equvin  1741  19.8a  1792  ax6e  1945  axc11n  1996  equvinOLD  2039  ax12vALT  2133  sbcom2  2153  euex  2279  mo3  2292  mo3OLD  2293  moOLD  2300  mopick  2336  mopickOLD  2337  gencl  2991  cgsexg  2994  gencbvex2  3006  vtocleg  3032  eqvinc  3075  elrabi  3103  sbcex2  3228  eluni  4082  intab  4146  uniintsn  4153  disjiun  4270  trint0  4390  bm1.3ii  4404  intex  4436  axpweq  4457  eunex  4473  eusvnf  4475  eusvnfb  4476  reusv2lem3  4483  unipw  4530  moabex  4539  nnullss  4542  exss  4543  mosubopt  4577  opelopabsb  4588  relop  4977  dmrnssfld  5085  dmsnopg  5298  unixp0  5359  iotauni  5381  iota1  5383  iota4  5387  dffv2  5752  eldmrexrnb  5838  exfo  5849  csbriota  6052  eusvobj2  6072  fnoprabg  6180  limuni3  6452  tfindsg  6460  findsg  6492  elxp5  6512  ffoss  6527  fo1stres  6589  fo2ndres  6590  eloprabi  6625  frxp  6671  suppimacnv  6690  mpt2xopxnop0  6721  reldmtpos  6742  dftpos4  6753  tfrlem9  6830  ecdmn0  7131  mapprc  7206  ixpprc  7272  ixpn0  7283  bren  7307  brdomg  7308  ener  7344  en0  7360  en1  7364  en1b  7365  2dom  7370  fiprc  7379  pwdom  7451  domssex  7460  ssenen  7473  php  7483  isinf  7514  findcard2s  7541  hartogslem1  7744  brwdom  7770  brwdomn0  7772  wdompwdom  7781  unxpwdom2  7791  ixpiunwdom  7794  inf3  7829  infeq5  7831  omex  7837  epfrs  7939  rankwflemb  7988  bnd2  8088  oncard  8118  carduni  8139  pm54.43  8158  ween  8193  acnrcl  8200  acndom  8209  acndom2  8212  iunfictbso  8272  aceq3lem  8278  dfac4  8280  dfac5lem4  8284  dfac5lem5  8285  dfac5  8286  dfac2a  8287  dfac2  8288  dfacacn  8298  dfac12r  8303  kmlem2  8308  kmlem16  8322  ackbij2  8400  cff  8405  cardcf  8409  cfeq0  8413  cfsuc  8414  cff1  8415  cfcoflem  8429  coftr  8430  infpssr  8465  fin4en1  8466  isfin4-2  8471  enfin2i  8478  fin23lem21  8496  fin23lem30  8499  fin23lem41  8509  enfin1ai  8541  fin1a2lem7  8563  axcc2lem  8593  domtriomlem  8599  dcomex  8604  axdc2lem  8605  axdc3lem2  8608  axdc4lem  8612  axcclem  8614  ac6s  8641  zorn2lem7  8659  ttukey2g  8673  axdclem2  8677  axdc  8678  brdom3  8683  brdom5  8684  brdom4  8685  brdom7disj  8686  brdom6disj  8687  konigthlem  8720  pwcfsdom  8735  pwfseq  8818  tsk0  8917  gruina  8972  grothpw  8980  grothpwex  8981  grothomex  8983  grothac  8984  ltbtwnnq  9134  reclem2pr  9204  supsrlem  9265  supsr  9266  axpre-sup  9323  dedekindle  9521  nnunb  10562  ioorebas  11378  fzn0  11450  fzon0  11552  axdc4uzlem  11787  hasheqf1oi  12105  hash1snb  12154  hashge3el3dif  12170  hashf1lem2  12192  brfi1uzind  12202  swrdcl  12298  fclim  13014  climmo  13018  rlimdmo1  13078  cnso  13511  xpsfrnel2  14485  brssc  14709  sscpwex  14710  grpidval  15414  subgint  15684  giclcl  15779  gicrcl  15780  gicsym  15781  gicen  15784  gicsubgen  15785  cntzssv  15825  giccyg  16355  subrgint  16810  lmiclcl  17072  lmicrcl  17073  lmicsym  17074  abvn0b  17295  lmiclbs  18107  lmisfree  18112  lmictra  18115  neitr  18625  cmpsub  18844  bwth  18854  bwthOLD  18855  iuncon  18873  2ndcsb  18894  elpt  18986  ptclsg  19029  hmphsym  19196  hmphen  19199  haushmphlem  19201  cmphmph  19202  conhmph  19203  reghmph  19207  nrmhmph  19208  hmphdis  19210  indishmph  19212  hmphen2  19213  ufldom  19376  alexsubALTlem2  19461  alexsubALT  19464  metustfbasOLD  19981  metustfbas  19982  iunmbl2  20879  ioorcl2  20893  ioorinv2  20896  opnmblALT  20924  mpfrcl  21369  pf1rcl  21399  plyssc  21552  aannenlem2  21679  aannenlem3  21680  mulog2sum  22670  tgldim0eq  22837  axcontlem4  23035  usgraedg4  23127  edgusgranbfin  23180  uvtx01vtx  23222  3v3e3cycl2  23372  eupath  23424  shintcli  24554  strlem1  25476  eqvincg  25681  rexunirn  25698  ctex  25831  cnvoprab  25846  prsdm  26197  prsrn  26198  0elsiga  26410  sigaclcu  26413  issgon  26419  insiga  26433  relexpindlem  27187  wfrlem2  27571  wfrlem3  27572  wfrlem4  27573  wfrlem9  27578  wfrlem12  27581  frrlem2  27615  frrlem3  27616  frrlem4  27617  frrlem5e  27622  frrlem11  27626  txpss3v  27755  pprodss4v  27761  elsingles  27795  fnimage  27806  funpartlem  27819  funpartfun  27820  dfrdg4  27827  colinearex  27937  wl-sbcom2d  28233  mblfinlem3  28271  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  indexdom  28469  prtlem16  28856  sbccomieg  28973  setindtr  29215  setindtrs  29216  dfac11  29257  lnmlmic  29283  gicabl  29296  isnumbasgrplem1  29299  iotain  29513  iotavalb  29526  sbiota1  29530  fnchoice  29593  stoweidlem59  29697  f1oexbi  29999  wlk0  30135  wlknwwlknsur  30187  wlkiswwlksur  30194  wwlknndef  30212  2spontn0vne  30249  clwwlknndef  30279  rusgrasn  30400  vdfrgra0  30457  vdgfrgra0  30458  usgn0fidegnn0  30465  frgrawopreglem2  30481  friendship  30558  iunconlem2  31370  bnj521  31427  bnj906  31622  bnj938  31629  bnj1018  31654  bnj1020  31655  bnj1125  31682  bnj1145  31683  bj-axc11nv  31879  bj-eunex  31937  bj-snglex  32046
  Copyright terms: Public domain W3C validator