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

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

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

This inference, along with its many variants such as rexlimdv 3217, 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 2023 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 2070 and ax-8 2160. (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 1922 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 2006 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  exlimiiv  2024  exlimivv  2025  equvinvOLD  2129  ax8  2164  ax9  2171  sbcom2  2607  euex  2656  mo3  2670  mopick  2699  gencl  3428  cgsexg  3431  gencbvex2  3444  vtocleg  3471  eqvincg  3522  elrabi  3553  sbcex2  3681  eluni  4629  intab  4695  uniintsn  4702  disjiun  4828  trintss  4958  intex  5009  axpweq  5031  eunex  5056  eusvnf  5058  eusvnfb  5059  reusv2lem3  5066  unipw  5105  moabex  5114  nnullss  5117  exss  5118  mosubopt  5162  opelopabsb  5177  relop  5471  dmrnssfld  5582  dmsnopg  5815  unixp0  5880  elsnxp  5888  iotauni  6073  iota1  6075  iota4  6079  dffv2  6489  fveqdmss  6573  eldmrexrnb  6585  exfo  6596  funop  6635  funopdmsn  6636  funsndifnop  6637  csbriota  6844  eusvobj2  6864  fnoprabg  6988  limuni3  7279  tfindsg  7287  findsg  7320  elxp5  7338  f1oexbi  7343  ffoss  7354  fo1stres  7421  fo2ndres  7422  eloprabi  7462  frxp  7518  suppimacnv  7537  mpt2xneldm  7570  mpt2xopxnop0  7573  reldmtpos  7592  dftpos4  7603  wfrlem2  7647  wfrlem3  7648  wfrlem4  7650  wfrlem4OLD  7651  wfrdmcl  7656  wfrlem12  7659  tfrlem9  7714  ecdmn0  8021  mapprc  8093  ixpprc  8163  ixpn0  8174  bren  8198  brdomg  8199  ctex  8204  ener  8236  en0  8252  en1  8256  en1b  8257  2dom  8262  fiprc  8275  pwdom  8348  domssex  8357  ssenen  8370  php  8380  isinf  8409  findcard2s  8437  hartogslem1  8683  brwdom  8708  brwdomn0  8710  wdompwdom  8719  unxpwdom2  8729  ixpiunwdom  8732  infeq5  8778  omex  8784  epfrs  8851  rankwflemb  8900  bnd2  9000  oncard  9066  carduni  9087  pm54.43  9106  ween  9138  acnrcl  9145  acndom  9154  acndom2  9157  iunfictbso  9217  aceq3lem  9223  dfac4  9225  dfac5lem4  9229  dfac5lem5  9230  dfac5  9231  dfac2a  9232  dfac2b  9233  dfac2OLD  9235  dfacacn  9245  dfac12r  9250  kmlem2  9255  kmlem16  9269  ackbij2  9347  cff  9352  cardcf  9356  cfeq0  9360  cfsuc  9361  cff1  9362  cfcoflem  9376  coftr  9377  infpssr  9412  fin4en1  9413  isfin4-2  9418  enfin2i  9425  fin23lem21  9443  fin23lem30  9446  fin23lem41  9456  enfin1ai  9488  fin1a2lem7  9510  domtriomlem  9546  axdc2lem  9552  axdc3lem2  9555  axdc4lem  9559  axcclem  9561  ac6s  9588  zorn2lem7  9606  ttukey2g  9620  axdc  9625  brdom3  9632  brdom5  9633  brdom4  9634  brdom7disj  9635  brdom6disj  9636  konigthlem  9672  pwcfsdom  9687  pwfseq  9768  tsk0  9867  gruina  9922  grothpw  9930  ltbtwnnq  10082  reclem2pr  10152  supsrlem  10214  supsr  10215  axpre-sup  10272  dedekindle  10483  nnunb  11551  ioorebas  12490  fzn0  12574  fzon0  12707  axdc4uzlem  13002  hasheqf1oi  13356  hash1snb  13420  hash1n0  13422  hashf1lem2  13453  hashle2pr  13472  hashge2el2difr  13476  hashge3el3dif  13481  fi1uzind  13492  brfi1indALT  13495  swrdcl  13638  relexpindlem  14022  fclim  14503  climmo  14507  rlimdmo1  14567  xpsfrnel2  16426  cicsym  16664  cictr  16665  brssc  16674  sscpwex  16675  initoid  16855  termoid  16856  initoeu1  16861  initoeu2lem1  16864  initoeu2  16866  termoeu1  16868  opifismgm  17459  grpidval  17461  dfgrp3e  17716  subgint  17816  giclcl  17912  gicrcl  17913  gicsym  17914  gicen  17917  gicsubgen  17918  cntzssv  17958  giccyg  18498  brric2  18945  ricgic  18946  subrgint  19002  lmiclcl  19273  lmicrcl  19274  lmicsym  19275  abvn0b  19507  mpfrcl  19722  ply1frcl  19887  pf1rcl  19917  lmiclbs  20382  lmisfree  20387  lmictra  20390  mat1scmat  20552  toprntopon  20939  topnex  21010  neitr  21194  cmpsub  21413  bwth  21423  iunconn  21441  2ndcsb  21462  unisngl  21540  elpt  21585  ptclsg  21628  hmphsym  21795  hmphen  21798  haushmphlem  21800  cmphmph  21801  connhmph  21802  reghmph  21806  nrmhmph  21807  hmphdis  21809  indishmph  21811  hmphen2  21812  ufldom  21975  alexsubALTlem2  22061  alexsubALT  22064  metustfbas  22571  iunmbl2  23534  ioorcl2  23549  ioorinv2  23552  opnmblALT  23580  plyssc  24166  aannenlem2  24294  mulog2sum  25436  istrkg2ld  25569  axcontlem4  26057  lfuhgr1v0e  26358  nbgr1vtx  26466  edgusgrnbfin  26487  cplgr1vlem  26549  cplgr1v  26550  fusgrn0degnn0  26619  g0wlk0  26772  wspthneq1eq2  26983  wlkswwlksf1o  27002  wlknwwlksnsurOLD  27013  wlkwwlksurOLD  27021  wwlksnndef  27038  wspthsnonn0vne  27053  eulerpath  27410  frgrwopreglem2  27484  friendship  27583  shintcli  28513  strlem1  29434  rexunirn  29654  cnvoprabOLD  29822  prsdm  30282  prsrn  30283  0elsiga  30499  sigaclcu  30502  issgon  30508  insiga  30522  omssubaddlem  30683  omssubadd  30684  bnj521  31125  bnj906  31320  bnj938  31327  bnj1018  31352  bnj1020  31353  bnj1125  31380  bnj1145  31381  mppspstlem  31788  frrlem2  32099  frrlem3  32100  frrlem4  32101  frrlem5e  32106  frrlem11  32110  sslttr  32232  txpss3v  32303  pprodss4v  32309  elsingles  32343  fnimage  32354  funpartlem  32367  funpartfun  32368  dfrdg4  32376  colinearex  32485  bj-sbex  32939  bj-cleljusti  32981  axc11n11r  32985  bj-eunex  33110  bj-mo3OLD  33142  bj-exlimvmpi  33210  bj-snglex  33268  bj-bm1.3ii  33331  bj-restpw  33353  mptsnunlem  33499  cnfinltrel  33554  wl-sbcom2d  33655  wl-mo3t  33669  wl-ax8clv1  33688  wl-ax8clv2  33691  ptrecube  33719  mblfinlem3  33758  ovoliunnfl  33761  voliunnfl  33763  volsupnfl  33764  indexdom  33838  xrnss3v  34444  prtlem16  34645  sbccomieg  37856  setindtr  38089  setindtrs  38090  dfac11  38130  lnmlmic  38156  gicabl  38167  isnumbasgrplem1  38169  rtrclex  38421  clcnvlem  38427  brtrclfv2  38516  snhesn  38577  frege55b  38688  frege55c  38709  iotain  39114  iotavalb  39127  sbiota1  39131  iunconnlem2  39662  fnchoice  39679  stoweidlem59  40752  vitali2  41387  nsssmfmbf  41466  funop1  41870  pfxcl  41958  opmpt2ismgm  42372  nzerooringczr  42637  setrec1lem3  43001  elsetrecs  43011  elpglem1  43022
  Copyright terms: Public domain W3C validator