Theorem exlimiv 1651

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v  1880  ax11ev  1881  equs5or  1883  exlimivv  1952  cbvexvw  1976  mo23  2128  mopick  2165  gencl  2854  cgsexg  2857  gencbvex2  2870  vtocleg  2896  eqvinc  2949  eqvincg  2950  elrabi  2979  sbcex2  3105  oprcl  3928  eluni  3938  intab  3999  uniintsnr  4006  trintssm  4247  bm1.3ii  4256  inteximm  4287  axpweq  4310  bnd2  4312  unipw  4359  euabex  4367  mss  4368  exss  4369  opelopabsb  4404  eusvnf  4601  eusvnfb  4602  regexmidlem1  4682  eunex  4710  relop  4932  dmrnssfld  5047  xpmlem  5211  dmxpss  5221  dmsnopg  5262  elxp5  5279  iotauni  5353  iota1  5355  iota4  5360  iotam  5372  funimaexglem  5467  ffoss  5675  relelfvdm  5730  elfvm  5732  nfvres  5735  fvelrnb  5753  funopsn  5894  funop  5895  funopdmsn  5898  mptmex  5948  eusvobj2  6074  acexmidlemv  6086  fnoprabg  6192  fo1stresm  6399  fo2ndresm  6400  eloprabi  6436  cnvoprab  6474  reldmtpos  6528  dftpos4  6538  tfrlem9  6594  tfrexlem  6609  ecdmn0m  6855  mapprc  6930  ixpprc  7005  ixpm  7016  bren  7034  brdomg  7036  domssr  7068  ener  7070  en0  7086  en1  7090  en1bg  7091  2dom  7097  fiprc  7108  dom1o  7120  enm  7122  ssenen  7156  php5dom  7168  ssfilem  7181  ssfilemd  7183  diffitest  7195  inffiexmid  7217  ctm  7455  ctssdclemr  7458  ctssdc  7459  enumct  7461  ctfoex  7464  ctssexmid  7496  pm54.43  7542  pr2cv1  7547  acnrcl  7563  subhalfnqq  7787  nqnq0pi  7811  nqnq0  7814  prarloc  7876  nqprm  7915  ltexprlemm  7973  recexprlemell  7995  recexprlemelu  7996  recexprlemopl  7998  recexprlemopu  8000  recexprlempr  8005  sup3exmid  9295  indval0  9306  fzm  10459  fzom  10589  hashf1lem2  11308  fclim  12085  climmo  12089  nninfct  12843  ctinfom  13377  qnnen  13380  unct  13391  omiunct  13393  opifismgmdc  13750  ismgmid  13756  gzsumval2  13773  ismnd  13791  dfgrp2e  13892  dfgrp3me  13964  subgintm  14060  cntrval  14151  cntzval  14153  cntzrcl  14159  resscntz  14166  mgpplusg  14329  mgpbas  14332  ringidval  14372  zrhval  15061  asclfval  15130  topnex  15312  edgval  16506  upgrex  16549  g0wlk0  16816  clwwlknonmpo  16874  bdbm1.3ii  17122  domomsubct  17236  wexmiddiffilem  17248  wexmiddifxylem  17250