Theorem exlimiv 1598

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 𝑥 exists satisfying a wff, i.e. ∃𝑥𝜑(𝑥) where 𝜑(𝑥) has 𝑥 free, then we can use 𝜑( 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 𝜑 (containing 𝑥) as an antecedent for the main part of the proof. We eventually arrive at (𝜑 → 𝜓) where 𝜓 is the theorem to be proved and does not contain 𝑥. Then we apply exlimiv 1598 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)

Hypothesis

Ref	Expression
exlimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimiv	⊢ (∃𝑥𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		ax-17 1526	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		exlimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	exlimih 1593	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1827  ax11ev  1828  equs5or  1830  exlimivv  1896  cbvexvw  1920  mo23  2067  mopick  2104  gencl  2769  cgsexg  2772  gencbvex2  2784  vtocleg  2808  eqvinc  2860  eqvincg  2861  elrabi  2890  sbcex2  3016  oprcl  3802  eluni  3812  intab  3873  uniintsnr  3880  trintssm  4117  bm1.3ii  4124  inteximm  4149  axpweq  4171  bnd2  4173  unipw  4217  euabex  4225  mss  4226  exss  4227  opelopabsb  4260  eusvnf  4453  eusvnfb  4454  regexmidlem1  4532  eunex  4560  relop  4777  dmrnssfld  4890  xpmlem  5049  dmxpss  5059  dmsnopg  5100  elxp5  5117  iotauni  5190  iota1  5192  iota4  5196  iotam  5208  funimaexglem  5299  ffoss  5493  relelfvdm  5547  nfvres  5548  fvelrnb  5563  eusvobj2  5860  acexmidlemv  5872  fnoprabg  5975  fo1stresm  6161  fo2ndresm  6162  eloprabi  6196  cnvoprab  6234  reldmtpos  6253  dftpos4  6263  tfrlem9  6319  tfrexlem  6334  ecdmn0m  6576  mapprc  6651  ixpprc  6718  ixpm  6729  bren  6746  brdomg  6747  ener  6778  en0  6794  en1  6798  en1bg  6799  2dom  6804  fiprc  6814  enm  6819  ssenen  6850  php5dom  6862  ssfilem  6874  diffitest  6886  inffiexmid  6905  ctm  7107  ctssdclemr  7110  ctssdc  7111  enumct  7113  ctfoex  7116  ctssexmid  7147  pm54.43  7188  subhalfnqq  7412  nqnq0pi  7436  nqnq0  7439  prarloc  7501  nqprm  7540  ltexprlemm  7598  recexprlemell  7620  recexprlemelu  7621  recexprlemopl  7623  recexprlemopu  7625  recexprlempr  7630  sup3exmid  8913  fzm  10037  fzom  10163  fclim  11301  climmo  11305  ctinfom  12428  qnnen  12431  unct  12442  omiunct  12444  opifismgmdc  12789  ismgmid  12795  ismnd  12819  dfgrp2e  12902  dfgrp3me  12969  subgintm  13056  topnex  13556  bdbm1.3ii  14613