Theorem exlimiv 1609

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 1609 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 1537	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1604	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1838  ax11ev  1839  equs5or  1841  exlimivv  1908  cbvexvw  1932  mo23  2083  mopick  2120  gencl  2792  cgsexg  2795  gencbvex2  2807  vtocleg  2831  eqvinc  2883  eqvincg  2884  elrabi  2913  sbcex2  3039  oprcl  3828  eluni  3838  intab  3899  uniintsnr  3906  trintssm  4143  bm1.3ii  4150  inteximm  4178  axpweq  4200  bnd2  4202  unipw  4246  euabex  4254  mss  4255  exss  4256  opelopabsb  4290  eusvnf  4484  eusvnfb  4485  regexmidlem1  4565  eunex  4593  relop  4812  dmrnssfld  4925  xpmlem  5086  dmxpss  5096  dmsnopg  5137  elxp5  5154  iotauni  5227  iota1  5229  iota4  5234  iotam  5246  funimaexglem  5337  ffoss  5532  relelfvdm  5586  elfvm  5587  nfvres  5588  fvelrnb  5604  eusvobj2  5904  acexmidlemv  5916  fnoprabg  6019  fo1stresm  6214  fo2ndresm  6215  eloprabi  6249  cnvoprab  6287  reldmtpos  6306  dftpos4  6316  tfrlem9  6372  tfrexlem  6387  ecdmn0m  6631  mapprc  6706  ixpprc  6773  ixpm  6784  bren  6801  brdomg  6802  ener  6833  en0  6849  en1  6853  en1bg  6854  2dom  6859  fiprc  6869  enm  6874  ssenen  6907  php5dom  6919  ssfilem  6931  diffitest  6943  inffiexmid  6962  ctm  7168  ctssdclemr  7171  ctssdc  7172  enumct  7174  ctfoex  7177  ctssexmid  7209  pm54.43  7250  subhalfnqq  7474  nqnq0pi  7498  nqnq0  7501  prarloc  7563  nqprm  7602  ltexprlemm  7660  recexprlemell  7682  recexprlemelu  7683  recexprlemopl  7685  recexprlemopu  7687  recexprlempr  7692  sup3exmid  8976  fzm  10104  fzom  10231  fclim  11437  climmo  11441  nninfct  12178  ctinfom  12585  qnnen  12588  unct  12599  omiunct  12601  opifismgmdc  12954  ismgmid  12960  gsumval2  12980  ismnd  13000  dfgrp2e  13100  dfgrp3me  13172  subgintm  13268  zrhval  14105  topnex  14254  bdbm1.3ii  15383