Theorem exlimiv 1622

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 1622 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 1550	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1617	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1851  ax11ev  1852  equs5or  1854  exlimivv  1921  cbvexvw  1945  mo23  2097  mopick  2134  gencl  2809  cgsexg  2812  gencbvex2  2825  vtocleg  2851  eqvinc  2903  eqvincg  2904  elrabi  2933  sbcex2  3059  oprcl  3857  eluni  3867  intab  3928  uniintsnr  3935  trintssm  4174  bm1.3ii  4181  inteximm  4209  axpweq  4231  bnd2  4233  unipw  4279  euabex  4287  mss  4288  exss  4289  opelopabsb  4324  eusvnf  4518  eusvnfb  4519  regexmidlem1  4599  eunex  4627  relop  4846  dmrnssfld  4960  xpmlem  5122  dmxpss  5132  dmsnopg  5173  elxp5  5190  iotauni  5263  iota1  5265  iota4  5270  iotam  5282  funimaexglem  5376  ffoss  5576  relelfvdm  5631  elfvm  5632  nfvres  5633  fvelrnb  5649  funopsn  5785  funop  5786  funopdmsn  5787  eusvobj2  5953  acexmidlemv  5965  fnoprabg  6069  fo1stresm  6270  fo2ndresm  6271  eloprabi  6305  cnvoprab  6343  reldmtpos  6362  dftpos4  6372  tfrlem9  6428  tfrexlem  6443  ecdmn0m  6687  mapprc  6762  ixpprc  6829  ixpm  6840  bren  6858  brdomg  6860  domssr  6892  ener  6894  en0  6910  en1  6914  en1bg  6915  2dom  6921  fiprc  6931  enm  6940  ssenen  6973  php5dom  6985  ssfilem  6998  diffitest  7010  inffiexmid  7029  ctm  7237  ctssdclemr  7240  ctssdc  7241  enumct  7243  ctfoex  7246  ctssexmid  7278  pm54.43  7324  pr2cv1  7329  acnrcl  7344  subhalfnqq  7562  nqnq0pi  7586  nqnq0  7589  prarloc  7651  nqprm  7690  ltexprlemm  7748  recexprlemell  7770  recexprlemelu  7771  recexprlemopl  7773  recexprlemopu  7775  recexprlempr  7780  sup3exmid  9065  fzm  10195  fzom  10322  fclim  11720  climmo  11724  nninfct  12477  ctinfom  12914  qnnen  12917  unct  12928  omiunct  12930  opifismgmdc  13318  ismgmid  13324  gsumval2  13344  ismnd  13366  dfgrp2e  13475  dfgrp3me  13547  subgintm  13649  zrhval  14494  topnex  14673  upgrex  15814  bdbm1.3ii  16026  dom1o  16128  domomsubct  16140