Theorem exlimiv 1598

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 1598 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 1526	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1593	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1827  ax11ev  1828  equs5or  1830  exlimivv  1896  cbvexvw  1920  mo23  2067  mopick  2104  gencl  2770  cgsexg  2773  gencbvex2  2785  vtocleg  2809  eqvinc  2861  eqvincg  2862  elrabi  2891  sbcex2  3017  oprcl  3803  eluni  3813  intab  3874  uniintsnr  3881  trintssm  4118  bm1.3ii  4125  inteximm  4150  axpweq  4172  bnd2  4174  unipw  4218  euabex  4226  mss  4227  exss  4228  opelopabsb  4261  eusvnf  4454  eusvnfb  4455  regexmidlem1  4533  eunex  4561  relop  4778  dmrnssfld  4891  xpmlem  5050  dmxpss  5060  dmsnopg  5101  elxp5  5118  iotauni  5191  iota1  5193  iota4  5197  iotam  5209  funimaexglem  5300  ffoss  5494  relelfvdm  5548  nfvres  5549  fvelrnb  5564  eusvobj2  5861  acexmidlemv  5873  fnoprabg  5976  fo1stresm  6162  fo2ndresm  6163  eloprabi  6197  cnvoprab  6235  reldmtpos  6254  dftpos4  6264  tfrlem9  6320  tfrexlem  6335  ecdmn0m  6577  mapprc  6652  ixpprc  6719  ixpm  6730  bren  6747  brdomg  6748  ener  6779  en0  6795  en1  6799  en1bg  6800  2dom  6805  fiprc  6815  enm  6820  ssenen  6851  php5dom  6863  ssfilem  6875  diffitest  6887  inffiexmid  6906  ctm  7108  ctssdclemr  7111  ctssdc  7112  enumct  7114  ctfoex  7117  ctssexmid  7148  pm54.43  7189  subhalfnqq  7413  nqnq0pi  7437  nqnq0  7440  prarloc  7502  nqprm  7541  ltexprlemm  7599  recexprlemell  7621  recexprlemelu  7622  recexprlemopl  7624  recexprlemopu  7626  recexprlempr  7631  sup3exmid  8914  fzm  10038  fzom  10164  fclim  11302  climmo  11306  ctinfom  12429  qnnen  12432  unct  12443  omiunct  12445  opifismgmdc  12790  ismgmid  12796  ismnd  12820  dfgrp2e  12903  dfgrp3me  12970  subgintm  13058  topnex  13589  bdbm1.3ii  14646