Theorem exlimiv 1634

Description: Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants such as rexlimdv 2738, 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/~hirstjl/primer/hirst.pdf 2738.

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 x exists satisfying a wff, i.e. ∃xφ(x) where φ(x) has x 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 x) 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 x. Then we apply exlimiv 1634 to arrive at (∃xφ → ψ). Finally, we separately prove ∃xφ and detach it with modus ponens ax-mp 5 to arrive at the final theorem ψ. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimiv.1	⊢ (φ → ψ)

Assertion

Ref	Expression
exlimiv	⊢ (∃xφ → ψ)

Distinct variable group:   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		exlimiv.1	. . 3 ⊢ (φ → ψ)
2	1	eximi 1576	. 2 ⊢ (∃xφ → ∃xψ)
3		ax17e 1618	. 2 ⊢ (∃xψ → ψ)
4	2, 3	syl 15	1 ⊢ (∃xφ → ψ)

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  exlimivv  1635  sp  1747  ax12olem1  1927  equvin  2001  ax11vALT  2097  mo  2226  mopick  2266  gencl  2888  cgsexg  2891  gencbvex2  2903  vtocleg  2926  eqvinc  2967  sbcex2  3096  eluni  3895  intab  3957  uniintsn  3964  unipw  4118  el1c  4140  pw10b  4167  ins2kss  4280  ins3kss  4281  cokrelk  4285  cnvkexg  4287  p6exg  4291  ssetkex  4295  sikexg  4297  ins2kexg  4306  ins3kexg  4307  eqpw1uni  4331  pw1eqadj  4333  sspw1  4336  sspw12  4337  iotauni  4352  iota1  4354  iota4  4358  0nelsuc  4401  nnsucelr  4429  sfintfin  4533  sfin111  4537  vfinspnn  4542  mosubopt  4613  phialllem2  4618  opelopabsb  4698  br1st  4859  br2nd  4860  brco  4884  dmcoss  4972  imasn  5019  ffoss  5315  fvprc  5326  fnoprabg  5586  op1st2nd  5791  addcfnex  5825  mapprc  6005  mapsspm  6022  mapsspw  6023  map0b  6025  map0  6026  bren  6031  ensymi  6037  en0  6043  enpw1  6063  enmap2  6069  enmap1  6075  elncs  6120  ncseqnc  6129  mucass  6136  1cnc  6140  muc0  6143  mucid1  6144  ce0  6191  nc0le1  6217  ce2lt  6221  lenc  6224  taddc  6230  letc  6232  ce0t  6233  cet  6235  tce2  6237  ce0lenc1  6240  tlenc1c  6241  addcdi  6251  spacssnc  6285