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  7271  acnrcl  7286  subhalfnqq  7500  nqnq0pi  7524  nqnq0  7527  prarloc  7589  nqprm  7628  ltexprlemm  7686  recexprlemell  7708  recexprlemelu  7709  recexprlemopl  7711  recexprlemopu  7713  recexprlempr  7718  sup3exmid  9003  fzm  10132  fzom  10259  fclim  11478  climmo  11482  nninfct  12235  ctinfom  12672  qnnen  12675  unct  12686  omiunct  12688  opifismgmdc  13075  ismgmid  13081  gsumval2  13101  ismnd  13123  dfgrp2e  13232  dfgrp3me  13304  subgintm  13406  zrhval  14251  topnex  14430  bdbm1.3ii  15645  domomsubct  15756