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

Theorem exlimiv 1645
Description: Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants such as rexlimdv 2835, 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.mathsci.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 (ficticious) 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 1645 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-9 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 1586 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax17e 1629 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 16 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551
This theorem is referenced by:  exlimivv  1646  19.8a  1764  a9e  1955  ax12olem1OLD  2014  ax10  2028  equvin  2090  ax11vALT  2179  mo  2309  mopick  2349  gencl  2990  cgsexg  2993  gencbvex2  3005  vtocleg  3028  eqvinc  3069  elrabi  3096  sbcex2  3219  eluni  4042  intab  4104  uniintsn  4111  disjiun  4227  trint0  4344  bm1.3ii  4358  intex  4385  axpweq  4405  eunex  4421  unipw  4443  moabex  4451  nnullss  4454  exss  4455  mosubopt  4483  opelopabsb  4494  eusvnf  4747  eusvnfb  4748  reusv2lem3  4755  limuni3  4861  tfindsg  4869  findsg  4901  relop  5052  dmrnssfld  5158  dmsnopg  5370  elxp5  5387  unixp0  5432  iotauni  5459  iota1  5461  iota4  5465  ffoss  5736  dffv2  5825  eldmrexrnb  5906  exfo  5916  fnoprabg  6200  fo1stres  6399  fo2ndres  6400  eloprabi  6442  frxp  6485  mpt2xopxnop0  6495  reldmtpos  6516  dftpos4  6527  eusvobj2  6611  tfrlem9  6675  ecdmn0  6976  mapprc  7051  ixpprc  7112  ixpn0  7123  bren  7146  brdomg  7147  ener  7183  en0  7199  en1  7203  en1b  7204  2dom  7208  fiprc  7217  pwdom  7288  domssex  7297  ssenen  7310  php  7320  isinf  7351  findcard2s  7378  hartogslem1  7540  brwdom  7564  brwdomn0  7566  wdompwdom  7575  unxpwdom2  7585  ixpiunwdom  7588  inf3  7619  infeq5  7621  omex  7627  epfrs  7696  rankwflemb  7748  bnd2  7848  oncard  7878  carduni  7899  pm54.43  7918  ween  7947  acnrcl  7954  acndom  7963  acndom2  7966  iunfictbso  8026  aceq3lem  8032  dfac4  8034  dfac5lem4  8038  dfac5lem5  8039  dfac5  8040  dfac2a  8041  dfac2  8042  dfacacn  8052  dfac12r  8057  kmlem2  8062  kmlem16  8076  ackbij2  8154  cff  8159  cardcf  8163  cfeq0  8167  cfsuc  8168  cff1  8169  cfcoflem  8183  coftr  8184  infpssr  8219  fin4en1  8220  isfin4-2  8225  enfin2i  8232  fin23lem21  8250  fin23lem30  8253  fin23lem41  8263  enfin1ai  8295  fin1a2lem7  8317  axcc2lem  8347  domtriomlem  8353  dcomex  8358  axdc2lem  8359  axdc3lem2  8362  axdc4lem  8366  axcclem  8368  ac6s  8395  zorn2lem7  8413  ttukey2g  8427  axdclem2  8431  axdc  8432  brdom3  8437  brdom5  8438  brdom4  8439  brdom7disj  8440  brdom6disj  8441  konigthlem  8474  pwcfsdom  8489  pwfseq  8570  tsk0  8669  gruina  8724  grothpw  8732  grothpwex  8733  grothomex  8735  grothac  8736  ltbtwnnq  8886  reclem2pr  8956  supsrlem  9017  supsr  9018  axpre-sup  9075  nnunb  10248  ioorebas  11037  fzn0  11101  fzon0  11187  axdc4uzlem  11352  hasheqf1oi  11666  hash1snb  11712  hashf1lem2  11736  brfi1uzind  11746  swrdcl  11797  fclim  12378  climmo  12382  rlimdmo1  12442  cnso  12877  xpsfrnel2  13821  brssc  14045  sscpwex  14046  grpidval  14738  subgint  14995  giclcl  15090  gicrcl  15091  gicsym  15092  gicen  15095  gicsubgen  15096  cntzssv  15158  giccyg  15540  subrgint  15921  lmiclcl  16173  lmicrcl  16174  lmicsym  16175  abvn0b  16393  neitr  17275  cmpsub  17494  bwth  17504  iuncon  17522  2ndcsb  17543  elpt  17635  ptclsg  17678  hmphsym  17845  hmphen  17848  haushmphlem  17850  cmphmph  17851  conhmph  17852  reghmph  17856  nrmhmph  17857  hmphdis  17859  indishmph  17861  hmphen2  17862  ufldom  18025  alexsubALTlem2  18110  alexsubALT  18113  metustfbasOLD  18626  metustfbas  18627  iunmbl2  19482  ioorcl2  19495  ioorinv2  19498  opnmblALT  19526  mpfrcl  19970  pf1rcl  20000  plyssc  20150  aannenlem2  20277  aannenlem3  20278  mulog2sum  21262  usgraedg4  21437  edgusgranbfin  21490  uvtx01vtx  21532  3v3e3cycl2  21682  eupath  21734  shintcli  22862  strlem1  23784  eqvincg  23992  rexunirn  24009  ctex  24131  0elsiga  24528  sigaclcu  24531  issgon  24537  insiga  24551  relexpindlem  25170  dedekindle  25219  wfrlem2  25570  wfrlem3  25571  wfrlem4  25572  wfrlem9  25577  wfrlem12  25580  frrlem2  25614  frrlem3  25615  frrlem4  25616  frrlem5e  25621  frrlem11  25625  txpss3v  25754  pprodss4v  25760  elsingles  25794  fnimage  25805  funpartlem  25818  funpartfun  25819  dfrdg4  25826  axcontlem4  25937  colinearex  26025  mblfinlem3  26281  ovoliunnfl  26284  voliunnfl  26286  volsupnfl  26287  indexdom  26474  prtlem16  26756  sbccomieg  26887  setindtr  27133  setindtrs  27134  dfac11  27175  lnmlmic  27201  gicabl  27278  isnumbasgrplem1  27281  lmiclbs  27322  lmisfree  27327  iotain  27632  iotavalb  27645  sbiota1  27649  fnchoice  27714  stoweidlem59  27822  2spontn0vne  28443  vdfrgra0  28510  vdgfrgra0  28511  frgrawopreglem2  28532  iunconlem2  29145  bnj521  29202  bnj906  29399  bnj938  29406  bnj1018  29431  bnj1020  29432  bnj1125  29459  bnj1145  29460  equvinNEW7  29627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator