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  2832  cgsexg  2835  gencbvex2  2848  vtocleg  2874  eqvinc  2926  eqvincg  2927  elrabi  2956  sbcex2  3082  oprcl  3880  eluni  3890  intab  3951  uniintsnr  3958  trintssm  4197  bm1.3ii  4204  inteximm  4232  axpweq  4254  bnd2  4256  unipw  4302  euabex  4310  mss  4311  exss  4312  opelopabsb  4347  eusvnf  4543  eusvnfb  4544  regexmidlem1  4624  eunex  4652  relop  4871  dmrnssfld  4986  xpmlem  5148  dmxpss  5158  dmsnopg  5199  elxp5  5216  iotauni  5290  iota1  5292  iota4  5297  iotam  5309  funimaexglem  5403  ffoss  5603  relelfvdm  5658  elfvm  5659  nfvres  5662  fvelrnb  5680  funopsn  5816  funop  5817  funopdmsn  5818  eusvobj2  5986  acexmidlemv  5998  fnoprabg  6104  fo1stresm  6305  fo2ndresm  6306  eloprabi  6340  cnvoprab  6378  reldmtpos  6397  dftpos4  6407  tfrlem9  6463  tfrexlem  6478  ecdmn0m  6722  mapprc  6797  ixpprc  6864  ixpm  6875  bren  6893  brdomg  6895  domssr  6927  ener  6929  en0  6945  en1  6949  en1bg  6950  2dom  6956  fiprc  6966  enm  6975  ssenen  7008  php5dom  7020  ssfilem  7033  diffitest  7045  inffiexmid  7064  ctm  7272  ctssdclemr  7275  ctssdc  7276  enumct  7278  ctfoex  7281  ctssexmid  7313  pm54.43  7359  pr2cv1  7364  acnrcl  7379  subhalfnqq  7597  nqnq0pi  7621  nqnq0  7624  prarloc  7686  nqprm  7725  ltexprlemm  7783  recexprlemell  7805  recexprlemelu  7806  recexprlemopl  7808  recexprlemopu  7810  recexprlempr  7815  sup3exmid  9100  fzm  10230  fzom  10357  fclim  11800  climmo  11804  nninfct  12557  ctinfom  12994  qnnen  12997  unct  13008  omiunct  13010  opifismgmdc  13399  ismgmid  13405  gsumval2  13425  ismnd  13447  dfgrp2e  13556  dfgrp3me  13628  subgintm  13730  zrhval  14575  topnex  14754  upgrex  15897  bdbm1.3ii  16212  dom1o  16314  domomsubct  16326