Theorem exlimiv 1577

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 1577 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 1506	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1572	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1799  ax11ev  1800  equs5or  1802  exlimivv  1868  mo23  2038  mopick  2075  gencl  2713  cgsexg  2716  gencbvex2  2728  vtocleg  2752  eqvinc  2803  eqvincg  2804  elrabi  2832  sbcex2  2957  oprcl  3724  eluni  3734  intab  3795  uniintsnr  3802  trintssm  4037  bm1.3ii  4044  inteximm  4069  axpweq  4090  bnd2  4092  unipw  4134  euabex  4142  mss  4143  exss  4144  opelopabsb  4177  eusvnf  4369  eusvnfb  4370  regexmidlem1  4443  eunex  4471  relop  4684  dmrnssfld  4797  xpmlem  4954  dmxpss  4964  dmsnopg  5005  elxp5  5022  iotauni  5095  iota1  5097  iota4  5101  funimaexglem  5201  ffoss  5392  relelfvdm  5446  nfvres  5447  fvelrnb  5462  eusvobj2  5753  acexmidlemv  5765  fnoprabg  5865  fo1stresm  6052  fo2ndresm  6053  eloprabi  6087  cnvoprab  6124  reldmtpos  6143  dftpos4  6153  tfrlem9  6209  tfrexlem  6224  ecdmn0m  6464  mapprc  6539  ixpprc  6606  ixpm  6617  bren  6634  brdomg  6635  ener  6666  en0  6682  en1  6686  en1bg  6687  2dom  6692  fiprc  6702  enm  6707  ssenen  6738  php5dom  6750  ssfilem  6762  diffitest  6774  inffiexmid  6793  ctm  6987  ctssdclemr  6990  ctssdc  6991  enumct  6993  ctfoex  6996  ctssexmid  7017  pm54.43  7039  subhalfnqq  7215  nqnq0pi  7239  nqnq0  7242  prarloc  7304  nqprm  7343  ltexprlemm  7401  recexprlemell  7423  recexprlemelu  7424  recexprlemopl  7426  recexprlemopu  7428  recexprlempr  7433  sup3exmid  8708  fzm  9811  fzom  9934  fclim  11056  climmo  11060  ctinfom  11930  qnnen  11933  unct  11943  topnex  12244  bdbm1.3ii  13078