Theorem exlimiv 1489

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 1489 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 7 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 1419	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		exlimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	exlimih 1484	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1338  ax-ie2 1383  ax-17 1419

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11v  1708  ax11ev  1709  equs5or  1711  exlimivv  1776  mo23  1941  mopick  1978  gencl  2586  cgsexg  2589  gencbvex2  2601  vtocleg  2624  eqvinc  2667  eqvincg  2668  elrabi  2695  sbcex2  2812  oprcl  3573  eluni  3583  intab  3644  uniintsnr  3651  trint0m  3871  bm1.3ii  3878  inteximm  3903  axpweq  3924  bnd2  3926  unipw  3953  euabex  3961  mss  3962  exss  3963  opelopabsb  3997  eusvnf  4185  eusvnfb  4186  regexmidlem1  4258  eunex  4285  relop  4486  dmrnssfld  4595  xpmlem  4744  dmxpss  4753  dmsnopg  4792  elxp5  4809  iotauni  4879  iota1  4881  iota4  4885  funimaexglem  4982  ffoss  5158  relelfvdm  5205  nfvres  5206  fvelrnb  5221  eusvobj2  5498  acexmidlemv  5510  fnoprabg  5602  fo1stresm  5788  fo2ndresm  5789  eloprabi  5822  reldmtpos  5868  dftpos4  5878  tfrlem9  5935  tfrexlem  5948  ecdmn0m  6148  bren  6228  brdomg  6229  ener  6259  en0  6275  en1  6279  en1bg  6280  2dom  6285  fiprc  6292  enm  6294  php5dom  6325  ssfiexmid  6336  diffitest  6344  subhalfnqq  6512  nqnq0pi  6536  nqnq0  6539  prarloc  6601  nqprm  6640  ltexprlemm  6698  recexprlemell  6720  recexprlemelu  6721  recexprlemopl  6723  recexprlemopu  6725  recexprlempr  6730  fzm  8902  fzom  9020  fclim  9815  climmo  9819  bdbm1.3ii  10011