Theorem exlimiv 1535

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 1535 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 7 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 1465	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		exlimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	exlimih 1530	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1427

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1384  ax-ie2 1429  ax-17 1465

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1756  ax11ev  1757  equs5or  1759  exlimivv  1825  mo23  1990  mopick  2027  gencl  2654  cgsexg  2657  gencbvex2  2669  vtocleg  2693  eqvinc  2743  eqvincg  2744  elrabi  2771  sbcex2  2895  oprcl  3654  eluni  3664  intab  3725  uniintsnr  3732  trintssm  3960  bm1.3ii  3968  inteximm  3993  axpweq  4014  bnd2  4016  unipw  4055  euabex  4063  mss  4064  exss  4065  opelopabsb  4098  eusvnf  4290  eusvnfb  4291  regexmidlem1  4364  eunex  4392  relop  4601  dmrnssfld  4711  xpmlem  4867  dmxpss  4876  dmsnopg  4917  elxp5  4934  iotauni  5007  iota1  5009  iota4  5013  funimaexglem  5112  ffoss  5300  relelfvdm  5351  nfvres  5352  fvelrnb  5367  eusvobj2  5654  acexmidlemv  5666  fnoprabg  5762  fo1stresm  5948  fo2ndresm  5949  eloprabi  5982  cnvoprab  6015  reldmtpos  6034  dftpos4  6044  tfrlem9  6100  tfrexlem  6115  ecdmn0m  6350  mapprc  6425  ixpprc  6492  ixpm  6503  bren  6520  brdomg  6521  ener  6552  en0  6568  en1  6572  en1bg  6573  2dom  6578  fiprc  6588  enm  6592  ssenen  6623  php5dom  6635  ssfilem  6647  diffitest  6659  inffiexmid  6678  ctm  6847  enumct  6849  pm54.43  6881  subhalfnqq  7036  nqnq0pi  7060  nqnq0  7063  prarloc  7125  nqprm  7164  ltexprlemm  7222  recexprlemell  7244  recexprlemelu  7245  recexprlemopl  7247  recexprlemopu  7249  recexprlempr  7254  fzm  9515  fzom  9638  fclim  10745  climmo  10749  topnex  11849  bdbm1.3ii  12086