Theorem exlimiv 1591

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 1591 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 1519	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		exlimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	exlimih 1586	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1820  ax11ev  1821  equs5or  1823  exlimivv  1889  cbvexvw  1913  mo23  2060  mopick  2097  gencl  2762  cgsexg  2765  gencbvex2  2777  vtocleg  2801  eqvinc  2853  eqvincg  2854  elrabi  2883  sbcex2  3008  oprcl  3789  eluni  3799  intab  3860  uniintsnr  3867  trintssm  4103  bm1.3ii  4110  inteximm  4135  axpweq  4157  bnd2  4159  unipw  4202  euabex  4210  mss  4211  exss  4212  opelopabsb  4245  eusvnf  4438  eusvnfb  4439  regexmidlem1  4517  eunex  4545  relop  4761  dmrnssfld  4874  xpmlem  5031  dmxpss  5041  dmsnopg  5082  elxp5  5099  iotauni  5172  iota1  5174  iota4  5178  iotam  5190  funimaexglem  5281  ffoss  5474  relelfvdm  5528  nfvres  5529  fvelrnb  5544  eusvobj2  5839  acexmidlemv  5851  fnoprabg  5954  fo1stresm  6140  fo2ndresm  6141  eloprabi  6175  cnvoprab  6213  reldmtpos  6232  dftpos4  6242  tfrlem9  6298  tfrexlem  6313  ecdmn0m  6555  mapprc  6630  ixpprc  6697  ixpm  6708  bren  6725  brdomg  6726  ener  6757  en0  6773  en1  6777  en1bg  6778  2dom  6783  fiprc  6793  enm  6798  ssenen  6829  php5dom  6841  ssfilem  6853  diffitest  6865  inffiexmid  6884  ctm  7086  ctssdclemr  7089  ctssdc  7090  enumct  7092  ctfoex  7095  ctssexmid  7126  pm54.43  7167  subhalfnqq  7376  nqnq0pi  7400  nqnq0  7403  prarloc  7465  nqprm  7504  ltexprlemm  7562  recexprlemell  7584  recexprlemelu  7585  recexprlemopl  7587  recexprlemopu  7589  recexprlempr  7594  sup3exmid  8873  fzm  9994  fzom  10120  fclim  11257  climmo  11261  ctinfom  12383  qnnen  12386  unct  12397  omiunct  12399  opifismgmdc  12625  ismgmid  12631  ismnd  12655  dfgrp2e  12733  topnex  12880  bdbm1.3ii  13926