Theorem exlimiv 1647

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

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1876  ax11ev  1877  equs5or  1879  exlimivv  1946  cbvexvw  1970  mo23  2122  mopick  2159  gencl  2846  cgsexg  2849  gencbvex2  2862  vtocleg  2888  eqvinc  2940  eqvincg  2941  elrabi  2970  sbcex2  3096  oprcl  3907  eluni  3917  intab  3978  uniintsnr  3985  trintssm  4224  bm1.3ii  4231  inteximm  4261  axpweq  4284  bnd2  4286  unipw  4333  euabex  4341  mss  4342  exss  4343  opelopabsb  4378  eusvnf  4574  eusvnfb  4575  regexmidlem1  4655  eunex  4683  relop  4905  dmrnssfld  5020  xpmlem  5183  dmxpss  5193  dmsnopg  5234  elxp5  5251  iotauni  5325  iota1  5327  iota4  5332  iotam  5344  funimaexglem  5439  ffoss  5647  relelfvdm  5702  elfvm  5703  nfvres  5706  fvelrnb  5724  funopsn  5860  funop  5861  funopdmsn  5864  eusvobj2  6036  acexmidlemv  6048  fnoprabg  6154  fo1stresm  6355  fo2ndresm  6356  eloprabi  6392  cnvoprab  6430  reldmtpos  6484  dftpos4  6494  tfrlem9  6550  tfrexlem  6565  ecdmn0m  6811  mapprc  6886  ixpprc  6954  ixpm  6965  bren  6983  brdomg  6985  domssr  7017  ener  7019  en0  7035  en1  7039  en1bg  7040  2dom  7046  fiprc  7057  dom1o  7069  enm  7071  ssenen  7105  php5dom  7117  ssfilem  7130  ssfilemd  7132  diffitest  7144  inffiexmid  7166  ctm  7400  ctssdclemr  7403  ctssdc  7404  enumct  7406  ctfoex  7409  ctssexmid  7441  pm54.43  7487  pr2cv1  7492  acnrcl  7508  subhalfnqq  7729  nqnq0pi  7753  nqnq0  7756  prarloc  7818  nqprm  7857  ltexprlemm  7915  recexprlemell  7937  recexprlemelu  7938  recexprlemopl  7940  recexprlemopu  7942  recexprlempr  7947  sup3exmid  9231  fzm  10372  fzom  10499  fclim  11979  climmo  11983  nninfct  12737  ctinfom  13179  qnnen  13182  unct  13193  omiunct  13195  opifismgmdc  13584  ismgmid  13590  gsumval2  13610  ismnd  13632  dfgrp2e  13741  dfgrp3me  13813  subgintm  13915  zrhval  14765  topnex  14951  edgval  16055  upgrex  16098  g0wlk0  16365  clwwlknonmpo  16423  bdbm1.3ii  16661  domomsubct  16775