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

Theorem exlimi 2233
Description: Inference associated with 19.23 2227. See exlimiv 2007 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 2227 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1874 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1853  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1854  df-nf 1859
This theorem is referenced by:  exlimih  2295  equs5aALT  2322  equs5eALT  2323  equsex  2437  nfeqf2  2442  exdistrf  2473  equs5a  2485  equs5e  2486  mo2v  2614  moanim  2667  euan  2668  moexex  2679  2eu6  2696  ceqsex  3381  sbhypf  3393  vtoclgf  3404  vtoclg1f  3405  vtoclef  3421  rspn0  4077  reusv2lem1  5017  copsexg  5104  copsex2g  5106  ralxpf  5424  dmcoss  5540  fv3  6367  tz6.12c  6374  opabiota  6423  0neqopab  6863  zfregcl  8664  scottex  8921  scott0  8922  dfac5lem5  9140  zfcndpow  9630  zfcndreg  9631  zfcndinf  9632  reclem2pr  10062  mreiincl  16458  brabgaf  29727  cnvoprabOLD  29807  bnj607  31293  bnj900  31306  exisym1  32729  exlimii  33124  bj-exlimmpi  33211  bj-exlimmpbi  33212  bj-exlimmpbir  33213  dihglblem5  37089  eu2ndop1stv  41708
  Copyright terms: Public domain W3C validator