Theorem exlimiv 1646

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 1646 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 1574	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1641	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1497  ax-ie2 1542  ax-17 1574

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  2835  cgsexg  2838  gencbvex2  2851  vtocleg  2877  eqvinc  2929  eqvincg  2930  elrabi  2959  sbcex2  3085  oprcl  3886  eluni  3896  intab  3957  uniintsnr  3964  trintssm  4203  bm1.3ii  4210  inteximm  4239  axpweq  4261  bnd2  4263  unipw  4309  euabex  4317  mss  4318  exss  4319  opelopabsb  4354  eusvnf  4550  eusvnfb  4551  regexmidlem1  4631  eunex  4659  relop  4880  dmrnssfld  4995  xpmlem  5157  dmxpss  5167  dmsnopg  5208  elxp5  5225  iotauni  5299  iota1  5301  iota4  5306  iotam  5318  funimaexglem  5413  ffoss  5616  relelfvdm  5671  elfvm  5672  nfvres  5675  fvelrnb  5693  funopsn  5830  funop  5831  funopdmsn  5834  eusvobj2  6004  acexmidlemv  6016  fnoprabg  6122  fo1stresm  6324  fo2ndresm  6325  eloprabi  6361  cnvoprab  6399  reldmtpos  6419  dftpos4  6429  tfrlem9  6485  tfrexlem  6500  ecdmn0m  6746  mapprc  6821  ixpprc  6888  ixpm  6899  bren  6917  brdomg  6919  domssr  6951  ener  6953  en0  6969  en1  6973  en1bg  6974  2dom  6980  fiprc  6990  dom1o  7002  enm  7004  ssenen  7037  php5dom  7049  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  ctm  7308  ctssdclemr  7311  ctssdc  7312  enumct  7314  ctfoex  7317  ctssexmid  7349  pm54.43  7395  pr2cv1  7400  acnrcl  7416  subhalfnqq  7634  nqnq0pi  7658  nqnq0  7661  prarloc  7723  nqprm  7762  ltexprlemm  7820  recexprlemell  7842  recexprlemelu  7843  recexprlemopl  7845  recexprlemopu  7847  recexprlempr  7852  sup3exmid  9137  fzm  10273  fzom  10400  fclim  11872  climmo  11876  nninfct  12630  ctinfom  13067  qnnen  13070  unct  13081  omiunct  13083  opifismgmdc  13472  ismgmid  13478  gsumval2  13498  ismnd  13520  dfgrp2e  13629  dfgrp3me  13701  subgintm  13803  zrhval  14650  topnex  14829  edgval  15930  upgrex  15973  g0wlk0  16240  clwwlknonmpo  16298  bdbm1.3ii  16537  domomsubct  16653