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

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

This inference, along with our many variants such as rexlimdv 2637, 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/~jlh/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 2024 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 10 to arrive at the final theorem  ps. (Contributed by NM, 5-Aug-1993.)

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 nfv 1629 . 2  |-  F/ x ps
2 exlimiv.1 . 2  |-  ( ph  ->  ps )
31, 2exlimi 1781 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  exlimivv  2026  mo  2138  mopick  2178  gencl  2767  cgsexg  2770  gencbvex2  2782  vtocleg  2805  eqvinc  2846  sbcex2  2984  eluni  3771  intab  3833  uniintsn  3840  disjiun  3953  trint0  4070  bm1.3ii  4084  intex  4109  axpweq  4125  eunex  4141  unipw  4162  moabex  4170  nnullss  4172  exss  4173  mosubopt  4201  opelopabsb  4212  eusvnf  4466  eusvnfb  4467  reusv2lem3  4474  limuni3  4580  tfindsg  4588  findsg  4620  relop  4787  dmrnssfld  4891  dmsnopg  5096  elxp5  5113  unixp0  5158  ffoss  5408  dffv2  5491  exfo  5577  fnoprabg  5844  fo1stres  6042  fo2ndres  6043  eloprabi  6085  frxp  6124  reldmtpos  6141  dftpos4  6152  iotauni  6202  iota1  6204  iota4  6208  eusvobj2  6270  tfrlem9  6334  ecdmn0  6635  mapprc  6709  ixpprc  6770  ixpn0  6781  bren  6804  brdomg  6805  ener  6841  en0  6857  en1  6861  en1b  6862  2dom  6866  fiprc  6875  pwdom  6946  domssex  6955  ssenen  6968  php  6978  isinf  7009  findcard2s  7032  hartogslem1  7190  brwdom  7214  brwdomn0  7216  wdompwdom  7225  unxpwdom2  7235  ixpiunwdom  7238  inf3  7269  infeq5  7271  omex  7277  epfrs  7346  rankwflemb  7398  bnd2  7496  oncard  7526  carduni  7547  pm54.43  7566  ween  7595  acnrcl  7602  acndom  7611  acndom2  7614  iunfictbso  7674  aceq3lem  7680  dfac4  7682  dfac5lem4  7686  dfac5lem5  7687  dfac5  7688  dfac2a  7689  dfac2  7690  dfacacn  7700  dfac12r  7705  kmlem2  7710  kmlem16  7724  ackbij2  7802  cff  7807  cardcf  7811  cfeq0  7815  cfsuc  7816  cff1  7817  cfcoflem  7831  coftr  7832  infpssr  7867  fin4en1  7868  isfin4-2  7873  enfin2i  7880  fin23lem21  7898  fin23lem30  7901  fin23lem41  7911  enfin1ai  7943  fin1a2lem7  7965  axcc2lem  7995  domtriomlem  8001  dcomex  8006  axdc2lem  8007  axdc3lem2  8010  axdc4lem  8014  axcclem  8016  ac6s  8044  zorn2lem7  8062  ttukey2g  8076  axdclem2  8080  axdc  8081  brdom3  8086  brdom5  8087  brdom4  8088  brdom7disj  8089  brdom6disj  8090  konigthlem  8123  pwcfsdom  8138  pwfseq  8219  tsk0  8318  gruina  8373  grothpw  8381  grothpwex  8382  grothomex  8384  grothac  8385  ltbtwnnq  8535  reclem2pr  8605  supsrlem  8666  supsr  8667  axpre-sup  8724  nnunb  9893  ioorebas  10676  fzn0  10740  fzon0  10822  axdc4uzlem  10975  hashf1lem2  11324  swrdcl  11382  fclim  11957  climmo  11961  rlimdmo1  12021  cnso  12452  xpsfrnel2  13394  brssc  13618  sscpwex  13619  grpidval  14311  subgint  14568  giclcl  14663  gicrcl  14664  gicsym  14665  gicen  14668  gicsubgen  14669  cntzssv  14731  giccyg  15113  subrgint  15494  lmiclcl  15750  lmicrcl  15751  lmicsym  15752  abvn0b  15970  cmpsub  17054  iuncon  17081  2ndcsb  17102  elpt  17194  ptclsg  17236  hmphsym  17400  hmphen  17403  haushmphlem  17405  cmphmph  17406  conhmph  17407  reghmph  17411  nrmhmph  17412  hmphdis  17414  indishmph  17416  hmphen2  17417  ufldom  17584  alexsubALTlem2  17669  alexsubALT  17672  iunmbl2  18841  ioorcl2  18854  ioorinv2  18857  opnmblALT  18885  mpfrcl  19329  pf1rcl  19359  plyssc  19509  aannenlem2  19636  aannenlem3  19637  mulog2sum  20613  shintcli  21833  strlem1  22755  eupath  23242  relexpindlem  23373  dedekindle  23419  wfrlem2  23591  wfrlem3  23592  wfrlem4  23593  wfrlem9  23598  wfrlem12  23601  frrlem2  23616  frrlem3  23617  frrlem4  23618  frrlem5e  23623  frrlem11  23627  txpss3v  23759  pprodss4v  23765  elfix  23784  dffix2  23786  elsingles  23797  fnimage  23808  funpartfun  23821  dfrdg4  23828  axcontlem4  23935  colinearex  24023  copsexgb  24297  prj1b  24410  prj3  24411  prl  24499  inposet  24610  osneisi  24863  dmhmph  24865  rnhmph  24866  fisub  24886  limptlimpr2lem1  24906  bwt2  24924  indexdom  25745  prtlem16  26069  sbccomieg  26202  setindtr  26449  setindtrs  26450  dfac11  26492  lnmlmic  26518  gicabl  26595  isnumbasgrplem1  26598  lmiclbs  26639  lmisfree  26644  iotain  26950  iotavalb  26963  sbiota1  26967  fnchoice  27033  stoweidlem53  27102  bnj521  27777  bnj906  27974  bnj938  27981  bnj1018  28006  bnj1020  28007  bnj1125  28034  bnj1145  28035
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator