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  3801  eluni  3811  intab  3872  uniintsnr  3879  trintssm  4115  bm1.3ii  4122  inteximm  4147  axpweq  4169  bnd2  4171  unipw  4215  euabex  4223  mss  4224  exss  4225  opelopabsb  4258  eusvnf  4451  eusvnfb  4452  regexmidlem1  4530  eunex  4558  relop  4774  dmrnssfld  4887  xpmlem  5046  dmxpss  5056  dmsnopg  5097  elxp5  5114  iotauni  5187  iota1  5189  iota4  5193  iotam  5205  funimaexglem  5296  ffoss  5490  relelfvdm  5544  nfvres  5545  fvelrnb  5560  eusvobj2  5856  acexmidlemv  5868  fnoprabg  5971  fo1stresm  6157  fo2ndresm  6158  eloprabi  6192  cnvoprab  6230  reldmtpos  6249  dftpos4  6259  tfrlem9  6315  tfrexlem  6330  ecdmn0m  6572  mapprc  6647  ixpprc  6714  ixpm  6725  bren  6742  brdomg  6743  ener  6774  en0  6790  en1  6794  en1bg  6795  2dom  6800  fiprc  6810  enm  6815  ssenen  6846  php5dom  6858  ssfilem  6870  diffitest  6882  inffiexmid  6901  ctm  7103  ctssdclemr  7106  ctssdc  7107  enumct  7109  ctfoex  7112  ctssexmid  7143  pm54.43  7184  subhalfnqq  7408  nqnq0pi  7432  nqnq0  7435  prarloc  7497  nqprm  7536  ltexprlemm  7594  recexprlemell  7616  recexprlemelu  7617  recexprlemopl  7619  recexprlemopu  7621  recexprlempr  7626  sup3exmid  8908  fzm  10031  fzom  10157  fclim  11293  climmo  11297  ctinfom  12419  qnnen  12422  unct  12433  omiunct  12435  opifismgmdc  12720  ismgmid  12726  ismnd  12750  dfgrp2e  12831  dfgrp3me  12898  subgintm  12984  topnex  13368  bdbm1.3ii  14414