Theorem exlimiv 1620

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

Syntax hints:   → wi 4  ∃wex 1514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1471  ax-ie2 1516  ax-17 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1849  ax11ev  1850  equs5or  1852  exlimivv  1919  cbvexvw  1943  mo23  2094  mopick  2131  gencl  2803  cgsexg  2806  gencbvex2  2819  vtocleg  2843  eqvinc  2895  eqvincg  2896  elrabi  2925  sbcex2  3051  oprcl  3842  eluni  3852  intab  3913  uniintsnr  3920  trintssm  4157  bm1.3ii  4164  inteximm  4192  axpweq  4214  bnd2  4216  unipw  4260  euabex  4268  mss  4269  exss  4270  opelopabsb  4304  eusvnf  4498  eusvnfb  4499  regexmidlem1  4579  eunex  4607  relop  4826  dmrnssfld  4939  xpmlem  5100  dmxpss  5110  dmsnopg  5151  elxp5  5168  iotauni  5241  iota1  5243  iota4  5248  iotam  5260  funimaexglem  5351  ffoss  5548  relelfvdm  5602  elfvm  5603  nfvres  5604  fvelrnb  5620  eusvobj2  5920  acexmidlemv  5932  fnoprabg  6036  fo1stresm  6237  fo2ndresm  6238  eloprabi  6272  cnvoprab  6310  reldmtpos  6329  dftpos4  6339  tfrlem9  6395  tfrexlem  6410  ecdmn0m  6654  mapprc  6729  ixpprc  6796  ixpm  6807  bren  6824  brdomg  6825  ener  6856  en0  6872  en1  6876  en1bg  6877  2dom  6882  fiprc  6892  enm  6897  ssenen  6930  php5dom  6942  ssfilem  6954  diffitest  6966  inffiexmid  6985  ctm  7193  ctssdclemr  7196  ctssdc  7197  enumct  7199  ctfoex  7202  ctssexmid  7234  pm54.43  7280  acnrcl  7295  subhalfnqq  7509  nqnq0pi  7533  nqnq0  7536  prarloc  7598  nqprm  7637  ltexprlemm  7695  recexprlemell  7717  recexprlemelu  7718  recexprlemopl  7720  recexprlemopu  7722  recexprlempr  7727  sup3exmid  9012  fzm  10142  fzom  10269  fclim  11524  climmo  11528  nninfct  12281  ctinfom  12718  qnnen  12721  unct  12732  omiunct  12734  opifismgmdc  13121  ismgmid  13127  gsumval2  13147  ismnd  13169  dfgrp2e  13278  dfgrp3me  13350  subgintm  13452  zrhval  14297  topnex  14476  bdbm1.3ii  15691  domomsubct  15802