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

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

This inference, along with our many variants such as rexlimdv 2628, 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 2023 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  2025  mo  2135  mopick  2175  gencl  2754  cgsexg  2757  gencbvex2  2769  vtocleg  2792  eqvinc  2832  sbcex2  2970  eluni  3730  intab  3790  uniintsn  3797  disjiun  3910  trint0  4027  bm1.3ii  4041  intex  4065  axpweq  4081  eunex  4097  unipw  4118  moabex  4126  nnullss  4128  exss  4129  mosubopt  4157  opelopabsb  4168  eusvnf  4420  eusvnfb  4421  reusv2lem3  4428  limuni3  4534  tfindsg  4542  findsg  4574  relop  4741  dmrnssfld  4845  dmsnopg  5050  elxp5  5067  unixp0  5112  ffoss  5362  dffv2  5444  exfo  5530  fnoprabg  5797  fo1stres  5995  fo2ndres  5996  eloprabi  6038  frxp  6077  reldmtpos  6094  dftpos4  6105  iotauni  6155  iota1  6157  iota4  6161  eusvobj2  6223  tfrlem9  6287  ecdmn0  6588  mapprc  6662  ixpprc  6723  ixpn0  6734  bren  6757  brdomg  6758  ener  6794  en0  6809  en1  6813  en1b  6814  2dom  6818  fiprc  6827  pwdom  6898  domssex  6907  ssenen  6920  php  6930  isinf  6961  findcard2s  6984  hartogslem1  7141  brwdom  7165  brwdomn0  7167  wdompwdom  7176  unxpwdom2  7186  ixpiunwdom  7189  inf3  7220  infeq5  7222  omex  7228  epfrs  7297  rankwflemb  7349  bnd2  7447  oncard  7477  carduni  7498  pm54.43  7517  ween  7546  acnrcl  7553  acndom  7562  acndom2  7565  iunfictbso  7625  aceq3lem  7631  dfac4  7633  dfac5lem4  7637  dfac5lem5  7638  dfac5  7639  dfac2a  7640  dfac2  7641  dfacacn  7651  dfac12r  7656  kmlem2  7661  kmlem16  7675  ackbij2  7753  cff  7758  cardcf  7762  cfeq0  7766  cfsuc  7767  cff1  7768  cfcoflem  7782  coftr  7783  infpssr  7818  fin4en1  7819  isfin4-2  7824  enfin2i  7831  fin23lem21  7849  fin23lem30  7852  fin23lem41  7862  enfin1ai  7894  fin1a2lem7  7916  axcc2lem  7946  domtriomlem  7952  dcomex  7957  axdc2lem  7958  axdc3lem2  7961  axdc4lem  7965  axcclem  7967  ac6s  7995  zorn2lem7  8013  ttukey2g  8027  axdclem2  8031  axdc  8032  brdom3  8037  brdom5  8038  brdom4  8039  brdom7disj  8040  brdom6disj  8041  konigthlem  8070  pwcfsdom  8085  pwfseq  8166  tsk0  8265  gruina  8320  grothpw  8328  grothpwex  8329  grothomex  8331  grothac  8332  ltbtwnnq  8482  reclem2pr  8552  supsrlem  8613  supsr  8614  axpre-sup  8671  nnunb  9840  ioorebas  10623  fzn0  10687  fzon0  10769  axdc4uzlem  10922  hashf1lem2  11271  swrdcl  11329  fclim  11904  climmo  11908  rlimdmo1  11968  cnso  12399  xpsfrnel2  13341  brssc  13535  sscpwex  13536  grpidval  14219  subgint  14476  giclcl  14571  gicrcl  14572  gicsym  14573  gicen  14576  gicsubgen  14577  cntzssv  14639  giccyg  15021  subrgint  15402  lmiclcl  15658  lmicrcl  15659  lmicsym  15660  abvn0b  15875  cmpsub  16959  iuncon  16986  2ndcsb  17007  elpt  17099  ptclsg  17141  hmphsym  17305  hmphen  17308  haushmphlem  17310  cmphmph  17311  conhmph  17312  reghmph  17316  nrmhmph  17317  hmphdis  17319  indishmph  17321  hmphen2  17322  ufldom  17489  alexsubALTlem2  17574  alexsubALT  17577  iunmbl2  18746  ioorcl2  18759  ioorinv2  18762  opnmblALT  18790  mpfrcl  19234  pf1rcl  19264  plyssc  19414  aannenlem2  19541  aannenlem3  19542  mulog2sum  20518  shintcli  21738  strlem1  22660  eupath  23076  relexpindlem  23207  dedekindle  23253  wfrlem2  23425  wfrlem3  23426  wfrlem4  23427  wfrlem9  23432  wfrlem12  23435  frrlem2  23450  frrlem3  23451  frrlem4  23452  frrlem5e  23457  frrlem11  23461  txpss3v  23593  pprodss4v  23599  elfix  23618  dffix2  23620  elsingles  23631  fnimage  23642  funpartfun  23655  dfrdg4  23662  axcontlem4  23769  colinearex  23857  copsexgb  24131  prj1b  24244  prj3  24245  prl  24333  inposet  24444  osneisi  24697  dmhmph  24699  rnhmph  24700  fisub  24720  limptlimpr2lem1  24740  bwt2  24758  indexdom  25579  prtlem16  25903  sbccomieg  26036  setindtr  26283  setindtrs  26284  dfac11  26326  lnmlmic  26352  gicabl  26429  isnumbasgrplem1  26432  lmiclbs  26473  lmisfree  26478  iotain  26784  iotavalb  26797  sbiota1  26801  bnj521  27454  bnj906  27651  bnj938  27658  bnj1018  27683  bnj1020  27684  bnj1125  27711  bnj1145  27712
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