Theorem exlimiv 1612

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

Syntax hints:   → wi 4  ∃wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1841  ax11ev  1842  equs5or  1844  exlimivv  1911  cbvexvw  1935  mo23  2086  mopick  2123  gencl  2795  cgsexg  2798  gencbvex2  2811  vtocleg  2835  eqvinc  2887  eqvincg  2888  elrabi  2917  sbcex2  3043  oprcl  3833  eluni  3843  intab  3904  uniintsnr  3911  trintssm  4148  bm1.3ii  4155  inteximm  4183  axpweq  4205  bnd2  4207  unipw  4251  euabex  4259  mss  4260  exss  4261  opelopabsb  4295  eusvnf  4489  eusvnfb  4490  regexmidlem1  4570  eunex  4598  relop  4817  dmrnssfld  4930  xpmlem  5091  dmxpss  5101  dmsnopg  5142  elxp5  5159  iotauni  5232  iota1  5234  iota4  5239  iotam  5251  funimaexglem  5342  ffoss  5539  relelfvdm  5593  elfvm  5594  nfvres  5595  fvelrnb  5611  eusvobj2  5911  acexmidlemv  5923  fnoprabg  6027  fo1stresm  6228  fo2ndresm  6229  eloprabi  6263  cnvoprab  6301  reldmtpos  6320  dftpos4  6330  tfrlem9  6386  tfrexlem  6401  ecdmn0m  6645  mapprc  6720  ixpprc  6787  ixpm  6798  bren  6815  brdomg  6816  ener  6847  en0  6863  en1  6867  en1bg  6868  2dom  6873  fiprc  6883  enm  6888  ssenen  6921  php5dom  6933  ssfilem  6945  diffitest  6957  inffiexmid  6976  ctm  7184  ctssdclemr  7187  ctssdc  7188  enumct  7190  ctfoex  7193  ctssexmid  7225  pm54.43  7269  acnrcl  7284  subhalfnqq  7498  nqnq0pi  7522  nqnq0  7525  prarloc  7587  nqprm  7626  ltexprlemm  7684  recexprlemell  7706  recexprlemelu  7707  recexprlemopl  7709  recexprlemopu  7711  recexprlempr  7716  sup3exmid  9001  fzm  10130  fzom  10257  fclim  11476  climmo  11480  nninfct  12233  ctinfom  12670  qnnen  12673  unct  12684  omiunct  12686  opifismgmdc  13073  ismgmid  13079  gsumval2  13099  ismnd  13121  dfgrp2e  13230  dfgrp3me  13302  subgintm  13404  zrhval  14249  topnex  14406  bdbm1.3ii  15621  domomsubct  15732