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

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

This inference, along with our many variants such as rexlimdv 2845, 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 1688 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.) (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 1625 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax5e 1672 . 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 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  exlimivv  1689  equvin  1742  19.8a  1793  ax6e  1946  axc11n  1997  equvinOLD  2040  ax12vALT  2131  sbcom2  2151  euex  2281  mo3  2298  mo3OLD  2299  moOLD  2305  mopick  2339  mopickOLD  2340  mopickOLDOLD  2341  gencl  3007  cgsexg  3010  gencbvex2  3022  vtocleg  3048  eqvinc  3091  elrabi  3119  sbcex2  3245  eluni  4099  intab  4163  uniintsn  4170  disjiun  4287  trint0  4407  bm1.3ii  4421  intex  4453  axpweq  4474  eunex  4490  eusvnf  4492  eusvnfb  4493  reusv2lem3  4500  unipw  4547  moabex  4556  nnullss  4559  exss  4560  mosubopt  4594  opelopabsb  4604  relop  4995  dmrnssfld  5103  dmsnopg  5315  unixp0  5376  iotauni  5398  iota1  5400  iota4  5404  dffv2  5769  eldmrexrnb  5855  exfo  5866  csbriota  6069  eusvobj2  6089  fnoprabg  6196  limuni3  6468  tfindsg  6476  findsg  6508  elxp5  6528  ffoss  6543  fo1stres  6605  fo2ndres  6606  eloprabi  6641  frxp  6687  suppimacnv  6706  mpt2xopxnop0  6737  reldmtpos  6758  dftpos4  6769  tfrlem9  6849  ecdmn0  7148  mapprc  7223  ixpprc  7289  ixpn0  7300  bren  7324  brdomg  7325  ener  7361  en0  7377  en1  7381  en1b  7382  2dom  7387  fiprc  7396  pwdom  7468  domssex  7477  ssenen  7490  php  7500  isinf  7531  findcard2s  7558  hartogslem1  7761  brwdom  7787  brwdomn0  7789  wdompwdom  7798  unxpwdom2  7808  ixpiunwdom  7811  inf3  7846  infeq5  7848  omex  7854  epfrs  7956  rankwflemb  8005  bnd2  8105  oncard  8135  carduni  8156  pm54.43  8175  ween  8210  acnrcl  8217  acndom  8226  acndom2  8229  iunfictbso  8289  aceq3lem  8295  dfac4  8297  dfac5lem4  8301  dfac5lem5  8302  dfac5  8303  dfac2a  8304  dfac2  8305  dfacacn  8315  dfac12r  8320  kmlem2  8325  kmlem16  8339  ackbij2  8417  cff  8422  cardcf  8426  cfeq0  8430  cfsuc  8431  cff1  8432  cfcoflem  8446  coftr  8447  infpssr  8482  fin4en1  8483  isfin4-2  8488  enfin2i  8495  fin23lem21  8513  fin23lem30  8516  fin23lem41  8526  enfin1ai  8558  fin1a2lem7  8580  axcc2lem  8610  domtriomlem  8616  dcomex  8621  axdc2lem  8622  axdc3lem2  8625  axdc4lem  8629  axcclem  8631  ac6s  8658  zorn2lem7  8676  ttukey2g  8690  axdclem2  8694  axdc  8695  brdom3  8700  brdom5  8701  brdom4  8702  brdom7disj  8703  brdom6disj  8704  konigthlem  8737  pwcfsdom  8752  pwfseq  8836  tsk0  8935  gruina  8990  grothpw  8998  grothpwex  8999  grothomex  9001  grothac  9002  ltbtwnnq  9152  reclem2pr  9222  supsrlem  9283  supsr  9284  axpre-sup  9341  dedekindle  9539  nnunb  10580  ioorebas  11396  fzn0  11469  fzon0  11574  axdc4uzlem  11809  hasheqf1oi  12127  hash1snb  12176  hashge3el3dif  12192  hashf1lem2  12214  brfi1uzind  12224  swrdcl  12320  fclim  13036  climmo  13040  rlimdmo1  13100  cnso  13534  xpsfrnel2  14508  brssc  14732  sscpwex  14733  grpidval  15437  subgint  15710  giclcl  15805  gicrcl  15806  gicsym  15807  gicen  15810  gicsubgen  15811  cntzssv  15851  giccyg  16381  subrgint  16892  lmiclcl  17156  lmicrcl  17157  lmicsym  17158  abvn0b  17379  mpfrcl  17609  ply1frcl  17758  pf1rcl  17788  lmiclbs  18271  lmisfree  18276  lmictra  18279  neitr  18789  cmpsub  19008  bwth  19018  bwthOLD  19019  iuncon  19037  2ndcsb  19058  elpt  19150  ptclsg  19193  hmphsym  19360  hmphen  19363  haushmphlem  19365  cmphmph  19366  conhmph  19367  reghmph  19371  nrmhmph  19372  hmphdis  19374  indishmph  19376  hmphen2  19377  ufldom  19540  alexsubALTlem2  19625  alexsubALT  19628  metustfbasOLD  20145  metustfbas  20146  iunmbl2  21043  ioorcl2  21057  ioorinv2  21060  opnmblALT  21088  plyssc  21673  aannenlem2  21800  aannenlem3  21801  mulog2sum  22791  tgldim0eq  22961  axcontlem4  23218  usgraedg4  23310  edgusgranbfin  23363  uvtx01vtx  23405  3v3e3cycl2  23555  eupath  23607  shintcli  24737  strlem1  25659  eqvincg  25864  rexunirn  25880  ctex  26013  cnvoprab  26028  prsdm  26349  prsrn  26350  0elsiga  26562  sigaclcu  26565  issgon  26571  insiga  26585  relexpindlem  27346  wfrlem2  27730  wfrlem3  27731  wfrlem4  27732  wfrlem9  27737  wfrlem12  27740  frrlem2  27774  frrlem3  27775  frrlem4  27776  frrlem5e  27781  frrlem11  27785  txpss3v  27914  pprodss4v  27920  elsingles  27954  fnimage  27965  funpartlem  27978  funpartfun  27979  dfrdg4  27986  colinearex  28096  wl-sbcom2d  28392  wl-mo3t  28402  mblfinlem3  28435  ovoliunnfl  28438  voliunnfl  28440  volsupnfl  28441  indexdom  28633  prtlem16  29019  sbccomieg  29136  setindtr  29378  setindtrs  29379  dfac11  29420  lnmlmic  29446  gicabl  29459  isnumbasgrplem1  29462  iotain  29676  iotavalb  29689  sbiota1  29693  fnchoice  29756  stoweidlem59  29859  f1oexbi  30161  wlk0  30297  wlknwwlknsur  30349  wlkiswwlksur  30356  wwlknndef  30374  2spontn0vne  30411  clwwlknndef  30441  rusgrasn  30562  vdfrgra0  30619  vdgfrgra0  30620  usgn0fidegnn0  30627  frgrawopreglem2  30643  friendship  30720  iunconlem2  31676  bnj521  31733  bnj906  31928  bnj938  31935  bnj1018  31960  bnj1020  31961  bnj1125  31988  bnj1145  31989  bj-axc11nv  32256  bj-eunex  32325  bj-snglex  32471
  Copyright terms: Public domain W3C validator