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

Theorem exlimiv 1769
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1968.

See exlimi 1970 for a more general version requiring more axioms.

This inference, along with its many variants such as rexlimdv 2922, 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 1769 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, 21-Jun-1993.) Remove dependencies on ax-6 1797 and ax-8 1872. (Revised by Wolf Lammen, 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 1703 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax5e 1753 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 17 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  exlimivv  1770  equid  1842  equvin  1856  ax12v  1908  ax12vOLD  1909  19.8a  1910  19.8aOLD  1911  ax6e  2058  axc11n  2105  axc11nOLD  2106  sbcom2  2241  euex  2292  mo3  2306  mopick  2334  mopickOLD  2335  axext3  2409  gencl  3117  cgsexg  3120  gencbvex2  3132  vtocleg  3158  eqvinc  3204  elrabi  3232  sbcex2  3356  eluni  4225  intab  4289  uniintsn  4296  disjiun  4417  trint0  4537  bm1.3ii  4551  intex  4581  axpweq  4602  eunex  4618  eusvnf  4620  eusvnfb  4621  reusv2lem3  4628  unipw  4672  moabex  4681  nnullss  4684  exss  4685  mosubopt  4719  opelopabsb  4731  relop  5005  dmrnssfld  5113  dmsnopg  5327  unixp0  5390  iotauni  5577  iota1  5579  iota4  5583  dffv2  5954  fveqdmss  6032  eldmrexrnb  6044  exfo  6055  csbriota  6279  eusvobj2  6298  fnoprabg  6411  limuni3  6693  tfindsg  6701  findsg  6734  elxp5  6752  f1oexbi  6757  ffoss  6768  fo1stres  6831  fo2ndres  6832  eloprabi  6869  frxp  6917  suppimacnv  6936  mpt2xopxnop0  6969  reldmtpos  6989  dftpos4  7000  wfrlem2  7044  wfrlem3  7045  wfrlem4  7047  wfrdmcl  7052  wfrlem12  7055  tfrlem9  7111  ecdmn0  7414  mapprc  7484  ixpprc  7551  ixpn0  7562  bren  7586  brdomg  7587  ener  7623  en0  7639  en1  7643  en1b  7644  2dom  7649  fiprc  7658  pwdom  7730  domssex  7739  ssenen  7752  php  7762  isinf  7791  findcard2s  7818  hartogslem1  8057  brwdom  8082  brwdomn0  8084  wdompwdom  8093  unxpwdom2  8103  ixpiunwdom  8106  inf3  8140  infeq5  8142  omex  8148  epfrs  8214  rankwflemb  8263  bnd2  8363  oncard  8393  carduni  8414  pm54.43  8433  ween  8464  acnrcl  8471  acndom  8480  acndom2  8483  iunfictbso  8543  aceq3lem  8549  dfac4  8551  dfac5lem4  8555  dfac5lem5  8556  dfac5  8557  dfac2a  8558  dfac2  8559  dfacacn  8569  dfac12r  8574  kmlem2  8579  kmlem16  8593  ackbij2  8671  cff  8676  cardcf  8680  cfeq0  8684  cfsuc  8685  cff1  8686  cfcoflem  8700  coftr  8701  infpssr  8736  fin4en1  8737  isfin4-2  8742  enfin2i  8749  fin23lem21  8767  fin23lem30  8770  fin23lem41  8780  enfin1ai  8812  fin1a2lem7  8834  axcc2lem  8864  domtriomlem  8870  dcomex  8875  axdc2lem  8876  axdc3lem2  8879  axdc4lem  8883  axcclem  8885  ac6s  8912  zorn2lem7  8930  ttukey2g  8944  axdclem2  8948  axdc  8949  brdom3  8954  brdom5  8955  brdom4  8956  brdom7disj  8957  brdom6disj  8958  konigthlem  8991  pwcfsdom  9006  pwfseq  9088  tsk0  9187  gruina  9242  grothpw  9250  grothpwex  9251  grothomex  9253  grothac  9254  ltbtwnnq  9402  reclem2pr  9472  supsrlem  9534  supsr  9535  axpre-sup  9592  dedekindle  9797  nnunb  10865  ioorebas  11736  fzn0  11811  fzon0  11935  axdc4uzlem  12192  hasheqf1oi  12531  hash1snb  12588  hashf1lem2  12614  hashge3el3dif  12633  brfi1uzind  12641  swrdcl  12760  relexpindlem  13105  fclim  13595  climmo  13599  rlimdmo1  13659  cnso  14277  xpsfrnel2  15413  cicsym  15651  cictr  15652  brssc  15661  sscpwex  15662  initoid  15842  termoid  15843  initoeu1  15848  initoeu2lem1  15851  initoeu2  15853  termoeu1  15855  opifismgm  16443  grpidval  16445  subgint  16783  giclcl  16878  gicrcl  16879  gicsym  16880  gicen  16883  gicsubgen  16884  cntzssv  16924  giccyg  17460  brric2  17899  ricgic  17900  subrgint  17956  lmiclcl  18219  lmicrcl  18220  lmicsym  18221  abvn0b  18452  mpfrcl  18667  ply1frcl  18833  pf1rcl  18863  lmiclbs  19317  lmisfree  19322  lmictra  19325  mat1scmat  19486  neitr  20118  cmpsub  20337  bwth  20347  iuncon  20365  2ndcsb  20386  unisngl  20464  elpt  20509  ptclsg  20552  hmphsym  20719  hmphen  20722  haushmphlem  20724  cmphmph  20725  conhmph  20726  reghmph  20730  nrmhmph  20731  hmphdis  20733  indishmph  20735  hmphen2  20736  ufldom  20899  alexsubALTlem2  20985  alexsubALT  20988  metustfbas  21494  iunmbl2  22378  ioorcl2  22392  ioorinv2  22395  ioorinv2OLD  22400  opnmblALT  22429  plyssc  23013  aannenlem2  23141  aannenlem3  23142  mulog2sum  24229  istrkg2ld  24362  axcontlem4  24834  usgraedg4  24951  edgusgranbfin  25014  uvtx01vtx  25056  3v3e3cycl2  25228  wlknwwlknsur  25276  wlkiswwlksur  25283  wwlknndef  25301  wlk0  25325  clwwlknndef  25337  2spontn0vne  25451  rusgrasn  25509  eupath  25545  vdfrgra0  25586  usgn0fidegnn0  25593  frgrawopreglem2  25609  friendship  25686  shintcli  26808  strlem1  27729  eqvincg  27934  rexunirn  27953  ctex  28126  cnvoprab  28142  prsdm  28550  prsrn  28551  0elsiga  28766  sigaclcu  28769  issgon  28775  insiga  28789  omssubaddlem  28951  omssubadd  28952  bnj521  29324  bnj906  29520  bnj938  29527  bnj1018  29552  bnj1020  29553  bnj1125  29580  bnj1145  29581  mppspstlem  29988  frrlem2  30293  frrlem3  30294  frrlem4  30295  frrlem5e  30300  frrlem11  30304  txpss3v  30421  pprodss4v  30427  elsingles  30461  fnimage  30472  funpartlem  30485  funpartfun  30486  dfrdg4  30494  colinearex  30603  bj-axc11nv  31087  bj-eunex  31156  bj-mo3OLD  31189  bj-snglex  31307  mptsnunlem  31465  wl-sbcom2d  31589  wl-mo3t  31599  wl-ax12v2  31603  wl-19.8a  31604  ptrecube  31634  mblfinlem3  31673  ovoliunnfl  31676  voliunnfl  31678  volsupnfl  31679  indexdom  31755  prtlem16  32139  sbccomieg  35335  setindtr  35575  setindtrs  35576  dfac11  35616  lnmlmic  35642  gicabl  35653  isnumbasgrplem1  35656  brtrclfv2  35948  snhesn  36009  frege55b  36120  frege55c  36141  iotain  36395  iotavalb  36408  sbiota1  36412  iunconlem2  36962  fnchoice  36980  stoweidlem59  37479  pfxcl  38307  opmpt2ismgm  38555  nzerooringczr  38822
  Copyright terms: Public domain W3C validator