MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimi Structured version   Visualization version   GIF version

Theorem exlimi 2070
Description: Inference associated with 19.23 2064. See exlimiv 1843 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exlimi.1 𝑥𝜓
exlimi.2 (𝜑𝜓)
Assertion
Ref Expression
exlimi (∃𝑥𝜑𝜓)

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3 𝑥𝜓
2119.23 2064 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1714 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-12 2031
This theorem depends on definitions:  df-bi 195  df-or 383  df-ex 1695  df-nf 1700
This theorem is referenced by:  exlimih  2130  equs5aALT  2159  equs5eALT  2160  equsex  2275  nfeqf2  2280  exdistrf  2316  equs5a  2331  equs5e  2332  mo2v  2460  moanim  2512  euan  2513  moexex  2524  2eu6  2541  ceqsex  3209  sbhypf  3221  vtoclgf  3232  vtoclg1f  3233  vtoclef  3249  rspn0  3887  reusv2lem1  4785  copsexg  4872  copsex2g  4874  ralxpf  5174  dmcoss  5289  fv3  6097  tz6.12c  6104  opabiota  6152  0neqopab  6570  zfregcl  8355  zfregclOLD  8357  scottex  8604  scott0  8605  dfac5lem5  8806  zfcndpow  9290  zfcndreg  9291  zfcndinf  9292  reclem2pr  9722  mreiincl  16021  brabgaf  28602  cnvoprab  28688  bnj607  30042  bnj900  30055  exisym1  31395  exlimii  31815  bj-exlimmpi  31896  bj-exlimmpbi  31897  bj-exlimmpbir  31898  dihglblem5  35404  eu2ndop1stv  39651
  Copyright terms: Public domain W3C validator