Theorem exlimiv 1644

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

Syntax hints:   -> wi 4   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1873  ax11ev  1874  equs5or  1876  exlimivv  1943  cbvexvw  1967  mo23  2119  mopick  2156  gencl  2832  cgsexg  2835  gencbvex2  2848  vtocleg  2874  eqvinc  2926  eqvincg  2927  elrabi  2956  sbcex2  3082  oprcl  3881  eluni  3891  intab  3952  uniintsnr  3959  trintssm  4198  bm1.3ii  4205  inteximm  4233  axpweq  4255  bnd2  4257  unipw  4303  euabex  4311  mss  4312  exss  4313  opelopabsb  4348  eusvnf  4544  eusvnfb  4545  regexmidlem1  4625  eunex  4653  relop  4872  dmrnssfld  4987  xpmlem  5149  dmxpss  5159  dmsnopg  5200  elxp5  5217  iotauni  5291  iota1  5293  iota4  5298  iotam  5310  funimaexglem  5404  ffoss  5604  relelfvdm  5659  elfvm  5660  nfvres  5663  fvelrnb  5681  funopsn  5817  funop  5818  funopdmsn  5819  eusvobj2  5987  acexmidlemv  5999  fnoprabg  6105  fo1stresm  6307  fo2ndresm  6308  eloprabi  6342  cnvoprab  6380  reldmtpos  6399  dftpos4  6409  tfrlem9  6465  tfrexlem  6480  ecdmn0m  6724  mapprc  6799  ixpprc  6866  ixpm  6877  bren  6895  brdomg  6897  domssr  6929  ener  6931  en0  6947  en1  6951  en1bg  6952  2dom  6958  fiprc  6968  dom1o  6977  enm  6979  ssenen  7012  php5dom  7024  ssfilem  7037  diffitest  7049  inffiexmid  7068  ctm  7276  ctssdclemr  7279  ctssdc  7280  enumct  7282  ctfoex  7285  ctssexmid  7317  pm54.43  7363  pr2cv1  7368  acnrcl  7383  subhalfnqq  7601  nqnq0pi  7625  nqnq0  7628  prarloc  7690  nqprm  7729  ltexprlemm  7787  recexprlemell  7809  recexprlemelu  7810  recexprlemopl  7812  recexprlemopu  7814  recexprlempr  7819  sup3exmid  9104  fzm  10234  fzom  10361  fclim  11805  climmo  11809  nninfct  12562  ctinfom  12999  qnnen  13002  unct  13013  omiunct  13015  opifismgmdc  13404  ismgmid  13410  gsumval2  13430  ismnd  13452  dfgrp2e  13561  dfgrp3me  13633  subgintm  13735  zrhval  14581  topnex  14760  upgrex  15903  g0wlk0  16081  bdbm1.3ii  16254  domomsubct  16367