Theorem exlimiv 1621

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 1621 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 1549	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1616	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1850  ax11ev  1851  equs5or  1853  exlimivv  1920  cbvexvw  1944  mo23  2095  mopick  2132  gencl  2804  cgsexg  2807  gencbvex2  2820  vtocleg  2844  eqvinc  2896  eqvincg  2897  elrabi  2926  sbcex2  3052  oprcl  3843  eluni  3853  intab  3914  uniintsnr  3921  trintssm  4159  bm1.3ii  4166  inteximm  4194  axpweq  4216  bnd2  4218  unipw  4262  euabex  4270  mss  4271  exss  4272  opelopabsb  4307  eusvnf  4501  eusvnfb  4502  regexmidlem1  4582  eunex  4610  relop  4829  dmrnssfld  4942  xpmlem  5104  dmxpss  5114  dmsnopg  5155  elxp5  5172  iotauni  5245  iota1  5247  iota4  5252  iotam  5264  funimaexglem  5358  ffoss  5556  relelfvdm  5610  elfvm  5611  nfvres  5612  fvelrnb  5628  funopsn  5764  funop  5765  funopdmsn  5766  eusvobj2  5932  acexmidlemv  5944  fnoprabg  6048  fo1stresm  6249  fo2ndresm  6250  eloprabi  6284  cnvoprab  6322  reldmtpos  6341  dftpos4  6351  tfrlem9  6407  tfrexlem  6422  ecdmn0m  6666  mapprc  6741  ixpprc  6808  ixpm  6819  bren  6837  brdomg  6839  domssr  6871  ener  6873  en0  6889  en1  6893  en1bg  6894  2dom  6899  fiprc  6909  enm  6917  ssenen  6950  php5dom  6962  ssfilem  6974  diffitest  6986  inffiexmid  7005  ctm  7213  ctssdclemr  7216  ctssdc  7217  enumct  7219  ctfoex  7222  ctssexmid  7254  pm54.43  7300  acnrcl  7315  subhalfnqq  7529  nqnq0pi  7553  nqnq0  7556  prarloc  7618  nqprm  7657  ltexprlemm  7715  recexprlemell  7737  recexprlemelu  7738  recexprlemopl  7740  recexprlemopu  7742  recexprlempr  7747  sup3exmid  9032  fzm  10162  fzom  10289  fclim  11638  climmo  11642  nninfct  12395  ctinfom  12832  qnnen  12835  unct  12846  omiunct  12848  opifismgmdc  13236  ismgmid  13242  gsumval2  13262  ismnd  13284  dfgrp2e  13393  dfgrp3me  13465  subgintm  13567  zrhval  14412  topnex  14591  bdbm1.3ii  15864  domomsubct  15975