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  3881  eluni  3891  intab  3952  uniintsnr  3959  trintssm  4198  bm1.3ii  4205  inteximm  4234  axpweq  4256  bnd2  4258  unipw  4304  euabex  4312  mss  4313  exss  4314  opelopabsb  4349  eusvnf  4545  eusvnfb  4546  regexmidlem1  4626  eunex  4654  relop  4875  dmrnssfld  4990  xpmlem  5152  dmxpss  5162  dmsnopg  5203  elxp5  5220  iotauni  5294  iota1  5296  iota4  5301  iotam  5313  funimaexglem  5407  ffoss  5609  relelfvdm  5664  elfvm  5665  nfvres  5668  fvelrnb  5686  funopsn  5822  funop  5823  funopdmsn  5826  eusvobj2  5996  acexmidlemv  6008  fnoprabg  6114  fo1stresm  6316  fo2ndresm  6317  eloprabi  6353  cnvoprab  6391  reldmtpos  6410  dftpos4  6420  tfrlem9  6476  tfrexlem  6491  ecdmn0m  6737  mapprc  6812  ixpprc  6879  ixpm  6890  bren  6908  brdomg  6910  domssr  6942  ener  6944  en0  6960  en1  6964  en1bg  6965  2dom  6971  fiprc  6981  dom1o  6990  enm  6992  ssenen  7025  php5dom  7037  ssfilem  7050  diffitest  7062  inffiexmid  7084  ctm  7292  ctssdclemr  7295  ctssdc  7296  enumct  7298  ctfoex  7301  ctssexmid  7333  pm54.43  7379  pr2cv1  7384  acnrcl  7399  subhalfnqq  7617  nqnq0pi  7641  nqnq0  7644  prarloc  7706  nqprm  7745  ltexprlemm  7803  recexprlemell  7825  recexprlemelu  7826  recexprlemopl  7828  recexprlemopu  7830  recexprlempr  7835  sup3exmid  9120  fzm  10251  fzom  10378  fclim  11826  climmo  11830  nninfct  12583  ctinfom  13020  qnnen  13023  unct  13034  omiunct  13036  opifismgmdc  13425  ismgmid  13431  gsumval2  13451  ismnd  13473  dfgrp2e  13582  dfgrp3me  13654  subgintm  13756  zrhval  14602  topnex  14781  upgrex  15924  g0wlk0  16142  bdbm1.3ii  16363  domomsubct  16480