Theorem exlimiv 1529

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

Syntax hints:   → wi 4  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1378  ax-ie2 1423  ax-17 1459

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11v  1748  ax11ev  1749  equs5or  1751  exlimivv  1817  mo23  1982  mopick  2019  gencl  2631  cgsexg  2634  gencbvex2  2646  vtocleg  2669  eqvinc  2718  eqvincg  2719  elrabi  2746  sbcex2  2867  oprcl  3594  eluni  3604  intab  3665  uniintsnr  3672  trintssm  3891  bm1.3ii  3899  inteximm  3924  axpweq  3945  bnd2  3947  unipw  3972  euabex  3980  mss  3981  exss  3982  opelopabsb  4015  eusvnf  4203  eusvnfb  4204  regexmidlem1  4276  eunex  4304  relop  4504  dmrnssfld  4613  xpmlem  4764  dmxpss  4773  dmsnopg  4812  elxp5  4829  iotauni  4899  iota1  4901  iota4  4905  funimaexglem  5002  ffoss  5178  relelfvdm  5226  nfvres  5227  fvelrnb  5242  eusvobj2  5518  acexmidlemv  5530  fnoprabg  5622  fo1stresm  5808  fo2ndresm  5809  eloprabi  5842  cnvoprab  5875  reldmtpos  5891  dftpos4  5901  tfrlem9  5958  tfrexlem  5971  ecdmn0m  6171  bren  6251  brdomg  6252  ener  6282  en0  6298  en1  6302  en1bg  6303  2dom  6308  fiprc  6315  enm  6317  php5dom  6349  ssfilem  6360  diffitest  6371  pm54.43  6459  subhalfnqq  6604  nqnq0pi  6628  nqnq0  6631  prarloc  6693  nqprm  6732  ltexprlemm  6790  recexprlemell  6812  recexprlemelu  6813  recexprlemopl  6815  recexprlemopu  6817  recexprlempr  6822  fzm  9057  fzom  9173  fclim  10133  climmo  10137  bdbm1.3ii  10682