Theorem exlimiv 1578

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 1578 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 1507	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1573	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1426  ax-ie2 1471  ax-17 1507

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1800  ax11ev  1801  equs5or  1803  exlimivv  1869  mo23  2041  mopick  2078  gencl  2721  cgsexg  2724  gencbvex2  2736  vtocleg  2760  eqvinc  2812  eqvincg  2813  elrabi  2841  sbcex2  2966  oprcl  3737  eluni  3747  intab  3808  uniintsnr  3815  trintssm  4050  bm1.3ii  4057  inteximm  4082  axpweq  4103  bnd2  4105  unipw  4147  euabex  4155  mss  4156  exss  4157  opelopabsb  4190  eusvnf  4382  eusvnfb  4383  regexmidlem1  4456  eunex  4484  relop  4697  dmrnssfld  4810  xpmlem  4967  dmxpss  4977  dmsnopg  5018  elxp5  5035  iotauni  5108  iota1  5110  iota4  5114  funimaexglem  5214  ffoss  5407  relelfvdm  5461  nfvres  5462  fvelrnb  5477  eusvobj2  5768  acexmidlemv  5780  fnoprabg  5880  fo1stresm  6067  fo2ndresm  6068  eloprabi  6102  cnvoprab  6139  reldmtpos  6158  dftpos4  6168  tfrlem9  6224  tfrexlem  6239  ecdmn0m  6479  mapprc  6554  ixpprc  6621  ixpm  6632  bren  6649  brdomg  6650  ener  6681  en0  6697  en1  6701  en1bg  6702  2dom  6707  fiprc  6717  enm  6722  ssenen  6753  php5dom  6765  ssfilem  6777  diffitest  6789  inffiexmid  6808  ctm  7002  ctssdclemr  7005  ctssdc  7006  enumct  7008  ctfoex  7011  ctssexmid  7032  pm54.43  7063  subhalfnqq  7246  nqnq0pi  7270  nqnq0  7273  prarloc  7335  nqprm  7374  ltexprlemm  7432  recexprlemell  7454  recexprlemelu  7455  recexprlemopl  7457  recexprlemopu  7459  recexprlempr  7464  sup3exmid  8739  fzm  9849  fzom  9972  fclim  11095  climmo  11099  ctinfom  11977  qnnen  11980  unct  11991  omiunct  11993  topnex  12294  bdbm1.3ii  13260