Theorem exlimiv 1644

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

Syntax hints:   → wi 4  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1873  ax11ev  1874  equs5or  1876  exlimivv  1943  cbvexvw  1967  mo23  2119  mopick  2156  gencl  2833  cgsexg  2836  gencbvex2  2849  vtocleg  2875  eqvinc  2927  eqvincg  2928  elrabi  2957  sbcex2  3083  oprcl  3884  eluni  3894  intab  3955  uniintsnr  3962  trintssm  4201  bm1.3ii  4208  inteximm  4237  axpweq  4259  bnd2  4261  unipw  4307  euabex  4315  mss  4316  exss  4317  opelopabsb  4352  eusvnf  4548  eusvnfb  4549  regexmidlem1  4629  eunex  4657  relop  4878  dmrnssfld  4993  xpmlem  5155  dmxpss  5165  dmsnopg  5206  elxp5  5223  iotauni  5297  iota1  5299  iota4  5304  iotam  5316  funimaexglem  5410  ffoss  5612  relelfvdm  5667  elfvm  5668  nfvres  5671  fvelrnb  5689  funopsn  5825  funop  5826  funopdmsn  5829  eusvobj2  5999  acexmidlemv  6011  fnoprabg  6117  fo1stresm  6319  fo2ndresm  6320  eloprabi  6356  cnvoprab  6394  reldmtpos  6414  dftpos4  6424  tfrlem9  6480  tfrexlem  6495  ecdmn0m  6741  mapprc  6816  ixpprc  6883  ixpm  6894  bren  6912  brdomg  6914  domssr  6946  ener  6948  en0  6964  en1  6968  en1bg  6969  2dom  6975  fiprc  6985  dom1o  6997  enm  6999  ssenen  7032  php5dom  7044  ssfilem  7057  diffitest  7069  inffiexmid  7091  ctm  7299  ctssdclemr  7302  ctssdc  7303  enumct  7305  ctfoex  7308  ctssexmid  7340  pm54.43  7386  pr2cv1  7391  acnrcl  7406  subhalfnqq  7624  nqnq0pi  7648  nqnq0  7651  prarloc  7713  nqprm  7752  ltexprlemm  7810  recexprlemell  7832  recexprlemelu  7833  recexprlemopl  7835  recexprlemopu  7837  recexprlempr  7842  sup3exmid  9127  fzm  10263  fzom  10390  fclim  11845  climmo  11849  nninfct  12602  ctinfom  13039  qnnen  13042  unct  13053  omiunct  13055  opifismgmdc  13444  ismgmid  13450  gsumval2  13470  ismnd  13492  dfgrp2e  13601  dfgrp3me  13673  subgintm  13775  zrhval  14621  topnex  14800  edgval  15901  upgrex  15944  g0wlk0  16167  clwwlknonmpo  16223  bdbm1.3ii  16422  domomsubct  16538