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

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

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

This inference, along with its many variants such as rexlimdv 3011, 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 𝐶 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 𝑥 exists satisfying a wff, i.e. 𝑥𝜑(𝑥) where 𝜑(𝑥) has 𝑥 free, then we can use 𝜑(𝐶) as a hypothesis for the proof where 𝐶 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 𝜑 (containing 𝑥) as an antecedent for the main part of the proof. We eventually arrive at (𝜑𝜓) where 𝜓 is the theorem to be proved and does not contain 𝑥. Then we apply exlimiv 1844 to arrive at (∃𝑥𝜑𝜓). Finally, we separately prove 𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1874 and ax-8 1978. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis
Ref Expression
exlimiv.1 (𝜑𝜓)
Assertion
Ref Expression
exlimiv (∃𝑥𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiv
StepHypRef Expression
1 exlimiv.1 . . 3 (𝜑𝜓)
21eximi 1751 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 1828 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  exlimiiv  1845  exlimivv  1846  equvinv  1945  equvinvOLD  1948  ax8  1982  ax9  1989  19.8aOLD  2039  sbcom2  2432  euex  2481  mo3  2494  mopick  2522  gencl  3207  cgsexg  3210  gencbvex2  3223  vtocleg  3251  eqvinc  3299  elrabi  3327  sbcex2  3452  eluni  4369  intab  4436  uniintsn  4443  disjiun  4567  trint0  4692  intex  4741  axpweq  4762  eunex  4779  eusvnf  4781  eusvnfb  4782  reusv2lem3  4791  unipw  4838  moabex  4847  nnullss  4850  exss  4851  mosubopt  4887  opelopabsb  4899  relop  5181  dmrnssfld  5291  dmsnopg  5509  unixp0  5571  elsnxp  5579  iotauni  5765  iota1  5767  iota4  5771  dffv2  6165  fveqdmss  6246  eldmrexrnb  6258  exfo  6269  csbriota  6500  eusvobj2  6519  fnoprabg  6636  limuni3  6921  tfindsg  6929  findsg  6962  elxp5  6981  f1oexbi  6986  ffoss  6997  fo1stres  7060  fo2ndres  7061  eloprabi  7098  frxp  7151  suppimacnv  7170  mpt2xneldm  7202  mpt2xopxnop0  7205  reldmtpos  7224  dftpos4  7235  wfrlem2  7279  wfrlem3  7280  wfrlem4  7282  wfrdmcl  7287  wfrlem12  7290  tfrlem9  7345  ecdmn0  7653  mapprc  7725  ixpprc  7792  ixpn0  7803  bren  7827  brdomg  7828  ctex  7833  ener  7865  enerOLD  7866  en0  7882  en1  7886  en1b  7887  2dom  7892  fiprc  7901  pwdom  7974  domssex  7983  ssenen  7996  php  8006  isinf  8035  findcard2s  8063  hartogslem1  8307  brwdom  8332  brwdomn0  8334  wdompwdom  8343  unxpwdom2  8353  ixpiunwdom  8356  infeq5  8394  omex  8400  epfrs  8467  rankwflemb  8516  bnd2  8616  oncard  8646  carduni  8667  pm54.43  8686  ween  8718  acnrcl  8725  acndom  8734  acndom2  8737  iunfictbso  8797  aceq3lem  8803  dfac4  8805  dfac5lem4  8809  dfac5lem5  8810  dfac5  8811  dfac2a  8812  dfac2  8813  dfacacn  8823  dfac12r  8828  kmlem2  8833  kmlem16  8847  ackbij2  8925  cff  8930  cardcf  8934  cfeq0  8938  cfsuc  8939  cff1  8940  cfcoflem  8954  coftr  8955  infpssr  8990  fin4en1  8991  isfin4-2  8996  enfin2i  9003  fin23lem21  9021  fin23lem30  9024  fin23lem41  9034  enfin1ai  9066  fin1a2lem7  9088  domtriomlem  9124  axdc2lem  9130  axdc3lem2  9133  axdc4lem  9137  axcclem  9139  ac6s  9166  zorn2lem7  9184  ttukey2g  9198  axdc  9203  brdom3  9208  brdom5  9209  brdom4  9210  brdom7disj  9211  brdom6disj  9212  konigthlem  9246  pwcfsdom  9261  pwfseq  9342  tsk0  9441  gruina  9496  grothpw  9504  ltbtwnnq  9656  reclem2pr  9726  supsrlem  9788  supsr  9789  axpre-sup  9846  dedekindle  10052  nnunb  11137  ioorebas  12104  fzn0  12183  fzon0  12313  axdc4uzlem  12601  hasheqf1oi  12956  hasheqf1oiOLD  12957  hash1snb  13022  hashf1lem2  13051  hashge2el2difr  13070  hashge3el3dif  13074  fi1uzind  13082  brfi1indALT  13085  fi1uzindOLD  13088  brfi1indALTOLD  13091  swrdcl  13219  relexpindlem  13599  fclim  14080  climmo  14084  rlimdmo1  14144  xpsfrnel2  15996  cicsym  16235  cictr  16236  brssc  16245  sscpwex  16246  initoid  16426  termoid  16427  initoeu1  16432  initoeu2lem1  16435  initoeu2  16437  termoeu1  16439  opifismgm  17029  grpidval  17031  dfgrp3e  17286  subgint  17389  giclcl  17485  gicrcl  17486  gicsym  17487  gicen  17491  gicsubgen  17492  cntzssv  17532  giccyg  18072  brric2  18516  ricgic  18517  subrgint  18573  lmiclcl  18839  lmicrcl  18840  lmicsym  18841  abvn0b  19071  mpfrcl  19287  ply1frcl  19452  pf1rcl  19482  lmiclbs  19942  lmisfree  19947  lmictra  19950  mat1scmat  20111  neitr  20741  cmpsub  20960  bwth  20970  iuncon  20988  2ndcsb  21009  unisngl  21087  elpt  21132  ptclsg  21175  hmphsym  21342  hmphen  21345  haushmphlem  21347  cmphmph  21348  conhmph  21349  reghmph  21353  nrmhmph  21354  hmphdis  21356  indishmph  21358  hmphen2  21359  ufldom  21523  alexsubALTlem2  21609  alexsubALT  21612  metustfbas  22119  iunmbl2  23076  ioorcl2  23090  ioorinv2  23093  opnmblALT  23121  plyssc  23704  aannenlem2  23832  mulog2sum  24970  istrkg2ld  25103  axcontlem4  25592  usgraedg4  25709  edgusgranbfin  25772  uvtx01vtx  25813  3v3e3cycl2  25985  wlknwwlknsur  26033  wlkiswwlksur  26040  wwlknndef  26058  wlk0  26082  clwwlknndef  26094  2spontn0vne  26207  rusgrasn  26265  eupath  26301  vdfrgra0  26342  usgn0fidegnn0  26349  frgrawopreglem2  26365  friendship  26442  shintcli  27365  strlem1  28286  eqvincg  28491  rexunirn  28508  cnvoprab  28679  prsdm  29081  prsrn  29082  0elsiga  29297  sigaclcu  29300  issgon  29306  insiga  29320  omssubaddlem  29481  omssubadd  29482  bnj521  29852  bnj906  30047  bnj938  30054  bnj1018  30079  bnj1020  30080  bnj1125  30107  bnj1145  30108  mppspstlem  30515  frrlem2  30818  frrlem3  30819  frrlem4  30820  frrlem5e  30825  frrlem11  30829  txpss3v  30948  pprodss4v  30954  elsingles  30988  fnimage  30999  funpartlem  31012  funpartfun  31013  dfrdg4  31021  colinearex  31130  bj-sbex  31608  bj-cleljusti  31649  axc11n11r  31653  bj-eunex  31780  bj-mo3OLD  31815  bj-snglex  31937  bj-restpw  32009  bj-toprntopon  32027  bj-topnex  32030  mptsnunlem  32144  wl-sbcom2d  32306  wl-mo3t  32320  ptrecube  32362  mblfinlem3  32401  ovoliunnfl  32404  voliunnfl  32406  volsupnfl  32407  indexdom  32482  prtlem16  32955  sbccomieg  36158  setindtr  36392  setindtrs  36393  dfac11  36433  lnmlmic  36459  gicabl  36470  isnumbasgrplem1  36473  rtrclex  36726  clcnvlem  36732  brtrclfv2  36821  snhesn  36883  frege55b  36994  frege55c  37015  iotain  37423  iotavalb  37436  sbiota1  37440  iunconlem2  37976  fnchoice  37994  stoweidlem59  38735  vitali2  39368  nsssmfmbf  39448  pfxcl  40033  funop  40124  funop1  40125  funsndifnop  40127  fundmge2nop0  40131  hash1n0  40177  lfuhgr1v0e  40461  nbgr1vtx  40561  edgusgrnbfin  40582  cplgr1vlem  40632  cplgr1v  40633  fusgrn0degnn0  40695  g01wlk0  40841  wspthneq1eq2  41037  1wlkpwwlkf1ouspgr  41057  wlknwwlksnsur  41068  wlkwwlksur  41075  wwlksnndef  41092  wspthsnonn0vne  41105  clwwlksnndef  41179  eulerpath  41390  frgrwopreglem2  41463  av-friendship  41534  opmpt2ismgm  41578  nzerooringczr  41845
  Copyright terms: Public domain W3C validator