Theorem exlimiv 1647

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 1647 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 1575	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1642	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1876  ax11ev  1877  equs5or  1879  exlimivv  1948  cbvexvw  1972  mo23  2124  mopick  2161  gencl  2848  cgsexg  2851  gencbvex2  2864  vtocleg  2890  eqvinc  2943  eqvincg  2944  elrabi  2973  sbcex2  3099  oprcl  3912  eluni  3922  intab  3983  uniintsnr  3990  trintssm  4229  bm1.3ii  4236  inteximm  4266  axpweq  4289  bnd2  4291  unipw  4338  euabex  4346  mss  4347  exss  4348  opelopabsb  4383  eusvnf  4579  eusvnfb  4580  regexmidlem1  4660  eunex  4688  relop  4910  dmrnssfld  5025  xpmlem  5188  dmxpss  5198  dmsnopg  5239  elxp5  5256  iotauni  5330  iota1  5332  iota4  5337  iotam  5349  funimaexglem  5444  ffoss  5652  relelfvdm  5707  elfvm  5708  nfvres  5711  fvelrnb  5729  funopsn  5865  funop  5866  funopdmsn  5869  eusvobj2  6044  acexmidlemv  6056  fnoprabg  6162  fo1stresm  6368  fo2ndresm  6369  eloprabi  6405  cnvoprab  6443  reldmtpos  6497  dftpos4  6507  tfrlem9  6563  tfrexlem  6578  ecdmn0m  6824  mapprc  6899  ixpprc  6967  ixpm  6978  bren  6996  brdomg  6998  domssr  7030  ener  7032  en0  7048  en1  7052  en1bg  7053  2dom  7059  fiprc  7070  dom1o  7082  enm  7084  ssenen  7118  php5dom  7130  ssfilem  7143  ssfilemd  7145  diffitest  7157  inffiexmid  7179  ctm  7413  ctssdclemr  7416  ctssdc  7417  enumct  7419  ctfoex  7422  ctssexmid  7454  pm54.43  7500  pr2cv1  7505  acnrcl  7521  subhalfnqq  7745  nqnq0pi  7769  nqnq0  7772  prarloc  7834  nqprm  7873  ltexprlemm  7931  recexprlemell  7953  recexprlemelu  7954  recexprlemopl  7956  recexprlemopu  7958  recexprlempr  7963  sup3exmid  9248  fzm  10392  fzom  10521  fclim  12004  climmo  12008  nninfct  12762  ctinfom  13263  qnnen  13266  unct  13277  omiunct  13279  opifismgmdc  13634  ismgmid  13640  gsumval2  13660  ismnd  13680  dfgrp2e  13783  dfgrp3me  13855  subgintm  13951  zrhval  14891  topnex  15077  edgval  16181  upgrex  16224  g0wlk0  16491  clwwlknonmpo  16549  bdbm1.3ii  16787  domomsubct  16901