Theorem exlimiv 1647

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

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1875  ax11ev  1876  equs5or  1878  exlimivv  1945  cbvexvw  1969  mo23  2121  mopick  2158  gencl  2836  cgsexg  2839  gencbvex2  2852  vtocleg  2878  eqvinc  2930  eqvincg  2931  elrabi  2960  sbcex2  3086  oprcl  3891  eluni  3901  intab  3962  uniintsnr  3969  trintssm  4208  bm1.3ii  4215  inteximm  4244  axpweq  4267  bnd2  4269  unipw  4315  euabex  4323  mss  4324  exss  4325  opelopabsb  4360  eusvnf  4556  eusvnfb  4557  regexmidlem1  4637  eunex  4665  relop  4886  dmrnssfld  5001  xpmlem  5164  dmxpss  5174  dmsnopg  5215  elxp5  5232  iotauni  5306  iota1  5308  iota4  5313  iotam  5325  funimaexglem  5420  ffoss  5625  relelfvdm  5680  elfvm  5681  nfvres  5684  fvelrnb  5702  funopsn  5838  funop  5839  funopdmsn  5842  eusvobj2  6014  acexmidlemv  6026  fnoprabg  6132  fo1stresm  6333  fo2ndresm  6334  eloprabi  6370  cnvoprab  6408  reldmtpos  6462  dftpos4  6472  tfrlem9  6528  tfrexlem  6543  ecdmn0m  6789  mapprc  6864  ixpprc  6931  ixpm  6942  bren  6960  brdomg  6962  domssr  6994  ener  6996  en0  7012  en1  7016  en1bg  7017  2dom  7023  fiprc  7033  dom1o  7045  enm  7047  ssenen  7080  php5dom  7092  ssfilem  7105  ssfilemd  7107  diffitest  7119  inffiexmid  7141  ctm  7351  ctssdclemr  7354  ctssdc  7355  enumct  7357  ctfoex  7360  ctssexmid  7392  pm54.43  7438  pr2cv1  7443  acnrcl  7459  subhalfnqq  7677  nqnq0pi  7701  nqnq0  7704  prarloc  7766  nqprm  7805  ltexprlemm  7863  recexprlemell  7885  recexprlemelu  7886  recexprlemopl  7888  recexprlemopu  7890  recexprlempr  7895  sup3exmid  9179  fzm  10318  fzom  10445  fclim  11917  climmo  11921  nninfct  12675  ctinfom  13112  qnnen  13115  unct  13126  omiunct  13128  opifismgmdc  13517  ismgmid  13523  gsumval2  13543  ismnd  13565  dfgrp2e  13674  dfgrp3me  13746  subgintm  13848  zrhval  14696  topnex  14880  edgval  15984  upgrex  16027  g0wlk0  16294  clwwlknonmpo  16352  bdbm1.3ii  16590  domomsubct  16706