Theorem exlimiv 1577

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

Syntax hints:   → wi 4  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1799  ax11ev  1800  equs5or  1802  exlimivv  1868  mo23  2040  mopick  2077  gencl  2718  cgsexg  2721  gencbvex2  2733  vtocleg  2757  eqvinc  2808  eqvincg  2809  elrabi  2837  sbcex2  2962  oprcl  3729  eluni  3739  intab  3800  uniintsnr  3807  trintssm  4042  bm1.3ii  4049  inteximm  4074  axpweq  4095  bnd2  4097  unipw  4139  euabex  4147  mss  4148  exss  4149  opelopabsb  4182  eusvnf  4374  eusvnfb  4375  regexmidlem1  4448  eunex  4476  relop  4689  dmrnssfld  4802  xpmlem  4959  dmxpss  4969  dmsnopg  5010  elxp5  5027  iotauni  5100  iota1  5102  iota4  5106  funimaexglem  5206  ffoss  5399  relelfvdm  5453  nfvres  5454  fvelrnb  5469  eusvobj2  5760  acexmidlemv  5772  fnoprabg  5872  fo1stresm  6059  fo2ndresm  6060  eloprabi  6094  cnvoprab  6131  reldmtpos  6150  dftpos4  6160  tfrlem9  6216  tfrexlem  6231  ecdmn0m  6471  mapprc  6546  ixpprc  6613  ixpm  6624  bren  6641  brdomg  6642  ener  6673  en0  6689  en1  6693  en1bg  6694  2dom  6699  fiprc  6709  enm  6714  ssenen  6745  php5dom  6757  ssfilem  6769  diffitest  6781  inffiexmid  6800  ctm  6994  ctssdclemr  6997  ctssdc  6998  enumct  7000  ctfoex  7003  ctssexmid  7024  pm54.43  7046  subhalfnqq  7222  nqnq0pi  7246  nqnq0  7249  prarloc  7311  nqprm  7350  ltexprlemm  7408  recexprlemell  7430  recexprlemelu  7431  recexprlemopl  7433  recexprlemopu  7435  recexprlempr  7440  sup3exmid  8715  fzm  9818  fzom  9941  fclim  11063  climmo  11067  ctinfom  11941  qnnen  11944  unct  11954  topnex  12255  bdbm1.3ii  13089