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  2808  vtocleg  2832  eqvinc  2884  eqvincg  2885  elrabi  2914  sbcex2  3040  oprcl  3829  eluni  3839  intab  3900  uniintsnr  3907  trintssm  4144  bm1.3ii  4151  inteximm  4179  axpweq  4201  bnd2  4203  unipw  4247  euabex  4255  mss  4256  exss  4257  opelopabsb  4291  eusvnf  4485  eusvnfb  4486  regexmidlem1  4566  eunex  4594  relop  4813  dmrnssfld  4926  xpmlem  5087  dmxpss  5097  dmsnopg  5138  elxp5  5155  iotauni  5228  iota1  5230  iota4  5235  iotam  5247  funimaexglem  5338  ffoss  5533  relelfvdm  5587  elfvm  5588  nfvres  5589  fvelrnb  5605  eusvobj2  5905  acexmidlemv  5917  fnoprabg  6020  fo1stresm  6216  fo2ndresm  6217  eloprabi  6251  cnvoprab  6289  reldmtpos  6308  dftpos4  6318  tfrlem9  6374  tfrexlem  6389  ecdmn0m  6633  mapprc  6708  ixpprc  6775  ixpm  6786  bren  6803  brdomg  6804  ener  6835  en0  6851  en1  6855  en1bg  6856  2dom  6861  fiprc  6871  enm  6876  ssenen  6909  php5dom  6921  ssfilem  6933  diffitest  6945  inffiexmid  6964  ctm  7170  ctssdclemr  7173  ctssdc  7174  enumct  7176  ctfoex  7179  ctssexmid  7211  pm54.43  7252  subhalfnqq  7476  nqnq0pi  7500  nqnq0  7503  prarloc  7565  nqprm  7604  ltexprlemm  7662  recexprlemell  7684  recexprlemelu  7685  recexprlemopl  7687  recexprlemopu  7689  recexprlempr  7694  sup3exmid  8978  fzm  10107  fzom  10234  fclim  11440  climmo  11444  nninfct  12181  ctinfom  12588  qnnen  12591  unct  12602  omiunct  12604  opifismgmdc  12957  ismgmid  12963  gsumval2  12983  ismnd  13003  dfgrp2e  13103  dfgrp3me  13175  subgintm  13271  zrhval  14116  topnex  14265  bdbm1.3ii  15453