Theorem exlimiv 1586

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 1586 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 1514	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1581	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1815  ax11ev  1816  equs5or  1818  exlimivv  1884  cbvexvw  1908  mo23  2055  mopick  2092  gencl  2758  cgsexg  2761  gencbvex2  2773  vtocleg  2797  eqvinc  2849  eqvincg  2850  elrabi  2879  sbcex2  3004  oprcl  3782  eluni  3792  intab  3853  uniintsnr  3860  trintssm  4096  bm1.3ii  4103  inteximm  4128  axpweq  4150  bnd2  4152  unipw  4195  euabex  4203  mss  4204  exss  4205  opelopabsb  4238  eusvnf  4431  eusvnfb  4432  regexmidlem1  4510  eunex  4538  relop  4754  dmrnssfld  4867  xpmlem  5024  dmxpss  5034  dmsnopg  5075  elxp5  5092  iotauni  5165  iota1  5167  iota4  5171  funimaexglem  5271  ffoss  5464  relelfvdm  5518  nfvres  5519  fvelrnb  5534  eusvobj2  5828  acexmidlemv  5840  fnoprabg  5943  fo1stresm  6129  fo2ndresm  6130  eloprabi  6164  cnvoprab  6202  reldmtpos  6221  dftpos4  6231  tfrlem9  6287  tfrexlem  6302  ecdmn0m  6543  mapprc  6618  ixpprc  6685  ixpm  6696  bren  6713  brdomg  6714  ener  6745  en0  6761  en1  6765  en1bg  6766  2dom  6771  fiprc  6781  enm  6786  ssenen  6817  php5dom  6829  ssfilem  6841  diffitest  6853  inffiexmid  6872  ctm  7074  ctssdclemr  7077  ctssdc  7078  enumct  7080  ctfoex  7083  ctssexmid  7114  pm54.43  7146  subhalfnqq  7355  nqnq0pi  7379  nqnq0  7382  prarloc  7444  nqprm  7483  ltexprlemm  7541  recexprlemell  7563  recexprlemelu  7564  recexprlemopl  7566  recexprlemopu  7568  recexprlempr  7573  sup3exmid  8852  fzm  9973  fzom  10099  fclim  11235  climmo  11239  ctinfom  12361  qnnen  12364  unct  12375  omiunct  12377  opifismgmdc  12602  ismgmid  12608  topnex  12726  bdbm1.3ii  13773