New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  exlimiv GIF version

Theorem exlimiv 1634
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. This inference, along with our many variants such as rexlimdv 2737, 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. 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 8 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
StepHypRef Expression
1 exlimiv.1 . . 3 (φψ)
21eximi 1576 . 2 (xφxψ)
3 ax17e 1618 . 2 (xψψ)
42, 3syl 15 1 (xφψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1541 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2887  cgsexg  2890  gencbvex2  2902  vtocleg  2925  eqvinc  2966  sbcex2  3095  eluni  3894  intab  3956  uniintsn  3963  unipw  4117  el1c  4139  pw10b  4166  ins2kss  4279  ins3kss  4280  cokrelk  4284  cnvkexg  4286  p6exg  4290  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  eqpw1uni  4330  pw1eqadj  4332  sspw1  4335  sspw12  4336  iotauni  4351  iota1  4353  iota4  4357  0nelsuc  4400  nnsucelr  4428  sfintfin  4532  sfin111  4536  vfinspnn  4541  mosubopt  4612  phialllem2  4617  opelopabsb  4697  br1st  4858  br2nd  4859  brco  4883  dmcoss  4971  imasn  5018  ffoss  5314  fvprc  5325  fnoprabg  5585  op1st2nd  5790  addcfnex  5824  mapprc  6004  mapsspm  6021  mapsspw  6022  map0b  6024  map0  6025  bren  6030  ensymi  6036  en0  6042  enpw1  6062  enmap2  6068  enmap1  6074  elncs  6119  ncseqnc  6128  mucass  6135  1cnc  6139  muc0  6142  mucid1  6143  ce0  6190  nc0le1  6216  ce2lt  6220  lenc  6223  taddc  6229  letc  6231  ce0t  6232  cet  6234  tce2  6236  ce0lenc1  6239  tlenc1c  6240  addcdi  6250  spacssnc  6284
 Copyright terms: Public domain W3C validator