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  4247  bm1.3ii  4256  inteximm  4287  axpweq  4310  bnd2  4312  unipw  4359  euabex  4367  mss  4368  exss  4369  opelopabsb  4404  eusvnf  4601  eusvnfb  4602  regexmidlem1  4682  eunex  4710  relop  4932  dmrnssfld  5047  xpmlem  5211  dmxpss  5221  dmsnopg  5262  elxp5  5279  iotauni  5353  iota1  5355  iota4  5360  iotam  5372  funimaexglem  5467  ffoss  5675  relelfvdm  5730  elfvm  5732  nfvres  5735  fvelrnb  5753  funopsn  5894  funop  5895  funopdmsn  5898  mptmex  5948  eusvobj2  6074  acexmidlemv  6086  fnoprabg  6192  fo1stresm  6399  fo2ndresm  6400  eloprabi  6436  cnvoprab  6474  reldmtpos  6529  dftpos4  6539  tfrlem9  6595  tfrexlem  6610  ecdmn0m  6856  mapprc  6931  ixpprc  7007  ixpm  7018  bren  7036  brdomg  7038  domssr  7070  ener  7072  en0  7088  en1  7092  en1bg  7093  2dom  7099  fiprc  7110  dom1o  7122  enm  7124  ssenen  7158  php5dom  7170  ssfilem  7183  ssfilemd  7185  diffitest  7197  inffiexmid  7219  ctm  7455  ctssdclemr  7458  ctssdc  7459  enumct  7461  ctfoex  7464  ctssexmid  7496  pm54.43  7542  pr2cv1  7547  acnrcl  7563  subhalfnqq  7787  nqnq0pi  7811  nqnq0  7814  prarloc  7876  nqprm  7915  ltexprlemm  7973  recexprlemell  7995  recexprlemelu  7996  recexprlemopl  7998  recexprlemopu  8000  recexprlempr  8005  sup3exmid  9295  indval0  9306  fzm  10458  fzom  10588  hashf1lem2  11307  fclim  12084  climmo  12088  nninfct  12842  ctinfom  13376  qnnen  13379  unct  13390  omiunct  13392  opifismgmdc  13749  ismgmid  13755  gzsumval2  13772  ismnd  13790  dfgrp2e  13891  dfgrp3me  13963  subgintm  14059  cntrval  14150  cntzval  14152  cntzrcl  14158  resscntz  14165  mgpplusg  14328  mgpbas  14331  ringidval  14371  zrhval  15060  asclfval  15129  topnex  15329  edgval  16523  upgrex  16566  g0wlk0  16833  clwwlknonmpo  16891  bdbm1.3ii  17139  domomsubct  17253  wexmiddiffilem  17265  wexmiddifxylem  17267