Theorem exlimiv 1647

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 1647 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 1575	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1642	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1875  ax11ev  1876  equs5or  1878  exlimivv  1945  cbvexvw  1969  mo23  2121  mopick  2158  gencl  2836  cgsexg  2839  gencbvex2  2852  vtocleg  2878  eqvinc  2930  eqvincg  2931  elrabi  2960  sbcex2  3086  oprcl  3891  eluni  3901  intab  3962  uniintsnr  3969  trintssm  4208  bm1.3ii  4215  inteximm  4244  axpweq  4267  bnd2  4269  unipw  4315  euabex  4323  mss  4324  exss  4325  opelopabsb  4360  eusvnf  4556  eusvnfb  4557  regexmidlem1  4637  eunex  4665  relop  4886  dmrnssfld  5001  xpmlem  5164  dmxpss  5174  dmsnopg  5215  elxp5  5232  iotauni  5306  iota1  5308  iota4  5313  iotam  5325  funimaexglem  5420  ffoss  5625  relelfvdm  5680  elfvm  5681  nfvres  5684  fvelrnb  5702  funopsn  5838  funop  5839  funopdmsn  5842  eusvobj2  6014  acexmidlemv  6026  fnoprabg  6132  fo1stresm  6333  fo2ndresm  6334  eloprabi  6370  cnvoprab  6408  reldmtpos  6462  dftpos4  6472  tfrlem9  6528  tfrexlem  6543  ecdmn0m  6789  mapprc  6864  ixpprc  6931  ixpm  6942  bren  6960  brdomg  6962  domssr  6994  ener  6996  en0  7012  en1  7016  en1bg  7017  2dom  7023  fiprc  7033  dom1o  7045  enm  7047  ssenen  7080  php5dom  7092  ssfilem  7105  ssfilemd  7107  diffitest  7119  inffiexmid  7141  ctm  7368  ctssdclemr  7371  ctssdc  7372  enumct  7374  ctfoex  7377  ctssexmid  7409  pm54.43  7455  pr2cv1  7460  acnrcl  7476  subhalfnqq  7694  nqnq0pi  7718  nqnq0  7721  prarloc  7783  nqprm  7822  ltexprlemm  7880  recexprlemell  7902  recexprlemelu  7903  recexprlemopl  7905  recexprlemopu  7907  recexprlempr  7912  sup3exmid  9196  fzm  10335  fzom  10462  fclim  11934  climmo  11938  nninfct  12692  ctinfom  13129  qnnen  13132  unct  13143  omiunct  13145  opifismgmdc  13534  ismgmid  13540  gsumval2  13560  ismnd  13582  dfgrp2e  13691  dfgrp3me  13763  subgintm  13865  zrhval  14713  topnex  14897  edgval  16001  upgrex  16044  g0wlk0  16311  clwwlknonmpo  16369  bdbm1.3ii  16607  domomsubct  16723