Theorem exlimiv 1651

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 1651 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 1579	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1646	1 |- ( E. x ph -> ps )

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v  1880  ax11ev  1881  equs5or  1883  exlimivv  1952  cbvexvw  1976  mo23  2128  mopick  2165  gencl  2854  cgsexg  2857  gencbvex2  2870  vtocleg  2896  eqvinc  2949  eqvincg  2950  elrabi  2979  sbcex2  3105  oprcl  3928  eluni  3938  intab  3999  uniintsnr  4006  trintssm  4245  bm1.3ii  4254  inteximm  4285  axpweq  4308  bnd2  4310  unipw  4357  euabex  4365  mss  4366  exss  4367  opelopabsb  4402  eusvnf  4599  eusvnfb  4600  regexmidlem1  4680  eunex  4708  relop  4930  dmrnssfld  5045  xpmlem  5208  dmxpss  5218  dmsnopg  5259  elxp5  5276  iotauni  5350  iota1  5352  iota4  5357  iotam  5369  funimaexglem  5464  ffoss  5672  relelfvdm  5727  elfvm  5729  nfvres  5732  fvelrnb  5750  funopsn  5891  funop  5892  funopdmsn  5895  mptmex  5945  eusvobj2  6071  acexmidlemv  6083  fnoprabg  6189  fo1stresm  6395  fo2ndresm  6396  eloprabi  6432  cnvoprab  6470  reldmtpos  6524  dftpos4  6534  tfrlem9  6590  tfrexlem  6605  ecdmn0m  6851  mapprc  6926  ixpprc  7001  ixpm  7012  bren  7030  brdomg  7032  domssr  7064  ener  7066  en0  7082  en1  7086  en1bg  7087  2dom  7093  fiprc  7104  dom1o  7116  enm  7118  ssenen  7152  php5dom  7164  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  ctm  7449  ctssdclemr  7452  ctssdc  7453  enumct  7455  ctfoex  7458  ctssexmid  7490  pm54.43  7536  pr2cv1  7541  acnrcl  7557  subhalfnqq  7781  nqnq0pi  7805  nqnq0  7808  prarloc  7870  nqprm  7909  ltexprlemm  7967  recexprlemell  7989  recexprlemelu  7990  recexprlemopl  7992  recexprlemopu  7994  recexprlempr  7999  sup3exmid  9287  indval0  9297  fzm  10442  fzom  10572  hashf1lem2  11286  fclim  12060  climmo  12064  nninfct  12818  ctinfom  13319  qnnen  13322  unct  13333  omiunct  13335  opifismgmdc  13691  ismgmid  13697  gzsumval2  13714  ismnd  13732  dfgrp2e  13833  dfgrp3me  13905  subgintm  14001  mgpplusg  14222  mgpbas  14225  ringidval  14265  zrhval  14952  asclfval  15021  topnex  15187  edgval  16301  upgrex  16344  g0wlk0  16611  clwwlknonmpo  16669  bdbm1.3ii  16917  domomsubct  17031  wexmiddiffilem  17043  wexmiddifxylem  17045