Theorem exlimiv 1621

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 1621 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 1549	. 2 |- ( ps -> A. x ps )
2		exlimiv.1	. 2 |- ( ph -> ps )
3	1, 2	exlimih 1616	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1850  ax11ev  1851  equs5or  1853  exlimivv  1920  cbvexvw  1944  mo23  2095  mopick  2132  gencl  2804  cgsexg  2807  gencbvex2  2820  vtocleg  2844  eqvinc  2896  eqvincg  2897  elrabi  2926  sbcex2  3052  oprcl  3843  eluni  3853  intab  3914  uniintsnr  3921  trintssm  4158  bm1.3ii  4165  inteximm  4193  axpweq  4215  bnd2  4217  unipw  4261  euabex  4269  mss  4270  exss  4271  opelopabsb  4306  eusvnf  4500  eusvnfb  4501  regexmidlem1  4581  eunex  4609  relop  4828  dmrnssfld  4941  xpmlem  5103  dmxpss  5113  dmsnopg  5154  elxp5  5171  iotauni  5244  iota1  5246  iota4  5251  iotam  5263  funimaexglem  5357  ffoss  5554  relelfvdm  5608  elfvm  5609  nfvres  5610  fvelrnb  5626  funopsn  5762  funop  5763  funopdmsn  5764  eusvobj2  5930  acexmidlemv  5942  fnoprabg  6046  fo1stresm  6247  fo2ndresm  6248  eloprabi  6282  cnvoprab  6320  reldmtpos  6339  dftpos4  6349  tfrlem9  6405  tfrexlem  6420  ecdmn0m  6664  mapprc  6739  ixpprc  6806  ixpm  6817  bren  6835  brdomg  6837  domssr  6869  ener  6871  en0  6887  en1  6891  en1bg  6892  2dom  6897  fiprc  6907  enm  6915  ssenen  6948  php5dom  6960  ssfilem  6972  diffitest  6984  inffiexmid  7003  ctm  7211  ctssdclemr  7214  ctssdc  7215  enumct  7217  ctfoex  7220  ctssexmid  7252  pm54.43  7298  acnrcl  7313  subhalfnqq  7527  nqnq0pi  7551  nqnq0  7554  prarloc  7616  nqprm  7655  ltexprlemm  7713  recexprlemell  7735  recexprlemelu  7736  recexprlemopl  7738  recexprlemopu  7740  recexprlempr  7745  sup3exmid  9030  fzm  10160  fzom  10287  fclim  11605  climmo  11609  nninfct  12362  ctinfom  12799  qnnen  12802  unct  12813  omiunct  12815  opifismgmdc  13203  ismgmid  13209  gsumval2  13229  ismnd  13251  dfgrp2e  13360  dfgrp3me  13432  subgintm  13534  zrhval  14379  topnex  14558  bdbm1.3ii  15827  domomsubct  15938