Theorem exlimiv 1598

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

Syntax hints:   → wi 4  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1827  ax11ev  1828  equs5or  1830  exlimivv  1896  cbvexvw  1920  mo23  2067  mopick  2104  gencl  2771  cgsexg  2774  gencbvex2  2786  vtocleg  2810  eqvinc  2862  eqvincg  2863  elrabi  2892  sbcex2  3018  oprcl  3804  eluni  3814  intab  3875  uniintsnr  3882  trintssm  4119  bm1.3ii  4126  inteximm  4151  axpweq  4173  bnd2  4175  unipw  4219  euabex  4227  mss  4228  exss  4229  opelopabsb  4262  eusvnf  4455  eusvnfb  4456  regexmidlem1  4534  eunex  4562  relop  4779  dmrnssfld  4892  xpmlem  5051  dmxpss  5061  dmsnopg  5102  elxp5  5119  iotauni  5192  iota1  5194  iota4  5198  iotam  5210  funimaexglem  5301  ffoss  5495  relelfvdm  5549  nfvres  5550  fvelrnb  5566  eusvobj2  5864  acexmidlemv  5876  fnoprabg  5979  fo1stresm  6165  fo2ndresm  6166  eloprabi  6200  cnvoprab  6238  reldmtpos  6257  dftpos4  6267  tfrlem9  6323  tfrexlem  6338  ecdmn0m  6580  mapprc  6655  ixpprc  6722  ixpm  6733  bren  6750  brdomg  6751  ener  6782  en0  6798  en1  6802  en1bg  6803  2dom  6808  fiprc  6818  enm  6823  ssenen  6854  php5dom  6866  ssfilem  6878  diffitest  6890  inffiexmid  6909  ctm  7111  ctssdclemr  7114  ctssdc  7115  enumct  7117  ctfoex  7120  ctssexmid  7151  pm54.43  7192  subhalfnqq  7416  nqnq0pi  7440  nqnq0  7443  prarloc  7505  nqprm  7544  ltexprlemm  7602  recexprlemell  7624  recexprlemelu  7625  recexprlemopl  7627  recexprlemopu  7629  recexprlempr  7634  sup3exmid  8917  fzm  10041  fzom  10167  fclim  11305  climmo  11309  ctinfom  12432  qnnen  12435  unct  12446  omiunct  12448  opifismgmdc  12796  ismgmid  12802  ismnd  12826  dfgrp2e  12909  dfgrp3me  12976  subgintm  13064  topnex  13726  bdbm1.3ii  14783