Theorem exlimiv 1612

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

Syntax hints:   → wi 4  ∃wex 1506

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1841  ax11ev  1842  equs5or  1844  exlimivv  1911  cbvexvw  1935  mo23  2086  mopick  2123  gencl  2795  cgsexg  2798  gencbvex2  2811  vtocleg  2835  eqvinc  2887  eqvincg  2888  elrabi  2917  sbcex2  3043  oprcl  3832  eluni  3842  intab  3903  uniintsnr  3910  trintssm  4147  bm1.3ii  4154  inteximm  4182  axpweq  4204  bnd2  4206  unipw  4250  euabex  4258  mss  4259  exss  4260  opelopabsb  4294  eusvnf  4488  eusvnfb  4489  regexmidlem1  4569  eunex  4597  relop  4816  dmrnssfld  4929  xpmlem  5090  dmxpss  5100  dmsnopg  5141  elxp5  5158  iotauni  5231  iota1  5233  iota4  5238  iotam  5250  funimaexglem  5341  ffoss  5536  relelfvdm  5590  elfvm  5591  nfvres  5592  fvelrnb  5608  eusvobj2  5908  acexmidlemv  5920  fnoprabg  6023  fo1stresm  6219  fo2ndresm  6220  eloprabi  6254  cnvoprab  6292  reldmtpos  6311  dftpos4  6321  tfrlem9  6377  tfrexlem  6392  ecdmn0m  6636  mapprc  6711  ixpprc  6778  ixpm  6789  bren  6806  brdomg  6807  ener  6838  en0  6854  en1  6858  en1bg  6859  2dom  6864  fiprc  6874  enm  6879  ssenen  6912  php5dom  6924  ssfilem  6936  diffitest  6948  inffiexmid  6967  ctm  7175  ctssdclemr  7178  ctssdc  7179  enumct  7181  ctfoex  7184  ctssexmid  7216  pm54.43  7257  subhalfnqq  7481  nqnq0pi  7505  nqnq0  7508  prarloc  7570  nqprm  7609  ltexprlemm  7667  recexprlemell  7689  recexprlemelu  7690  recexprlemopl  7692  recexprlemopu  7694  recexprlempr  7699  sup3exmid  8984  fzm  10113  fzom  10240  fclim  11459  climmo  11463  nninfct  12208  ctinfom  12645  qnnen  12648  unct  12659  omiunct  12661  opifismgmdc  13014  ismgmid  13020  gsumval2  13040  ismnd  13060  dfgrp2e  13160  dfgrp3me  13232  subgintm  13328  zrhval  14173  topnex  14322  bdbm1.3ii  15537