Theorem exlimiv 1651

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

This inference, along with our many variants 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 1651 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 NM, 25-Jul-2012.)

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

Step	Hyp	Ref	Expression
1		ax-17 1579	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1646	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1880  ax11ev  1881  equs5or  1883  exlimivv  1952  cbvexvw  1976  mo23  2128  mopick  2165  gencl  2854  cgsexg  2857  gencbvex2  2870  vtocleg  2896  eqvinc  2949  eqvincg  2950  elrabi  2979  sbcex2  3105  oprcl  3923  eluni  3933  intab  3994  uniintsnr  4001  trintssm  4240  bm1.3ii  4249  inteximm  4280  axpweq  4303  bnd2  4305  unipw  4352  euabex  4360  mss  4361  exss  4362  opelopabsb  4397  eusvnf  4594  eusvnfb  4595  regexmidlem1  4675  eunex  4703  relop  4925  dmrnssfld  5040  xpmlem  5203  dmxpss  5213  dmsnopg  5254  elxp5  5271  iotauni  5345  iota1  5347  iota4  5352  iotam  5364  funimaexglem  5459  ffoss  5667  relelfvdm  5722  elfvm  5723  nfvres  5726  fvelrnb  5744  funopsn  5882  funop  5883  funopdmsn  5886  eusvobj2  6061  acexmidlemv  6073  fnoprabg  6179  fo1stresm  6385  fo2ndresm  6386  eloprabi  6422  cnvoprab  6460  reldmtpos  6514  dftpos4  6524  tfrlem9  6580  tfrexlem  6595  ecdmn0m  6841  mapprc  6916  ixpprc  6991  ixpm  7002  bren  7020  brdomg  7022  domssr  7054  ener  7056  en0  7072  en1  7076  en1bg  7077  2dom  7083  fiprc  7094  dom1o  7106  enm  7108  ssenen  7142  php5dom  7154  ssfilem  7167  ssfilemd  7169  diffitest  7181  inffiexmid  7203  ctm  7439  ctssdclemr  7442  ctssdc  7443  enumct  7445  ctfoex  7448  ctssexmid  7480  pm54.43  7526  pr2cv1  7531  acnrcl  7547  subhalfnqq  7771  nqnq0pi  7795  nqnq0  7798  prarloc  7860  nqprm  7899  ltexprlemm  7957  recexprlemell  7979  recexprlemelu  7980  recexprlemopl  7982  recexprlemopu  7984  recexprlempr  7989  sup3exmid  9277  fzm  10421  fzom  10550  hashf1lem2  11264  fclim  12038  climmo  12042  nninfct  12796  ctinfom  13297  qnnen  13300  unct  13311  omiunct  13313  opifismgmdc  13668  ismgmid  13674  gzsumval2  13691  ismnd  13709  dfgrp2e  13810  dfgrp3me  13882  subgintm  13978  zrhval  14924  topnex  15110  edgval  16215  upgrex  16258  g0wlk0  16525  clwwlknonmpo  16583  bdbm1.3ii  16831  domomsubct  16945