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

Theorem exlimi 2253
Description: Inference associated with 19.23 2247. See exlimiv 2021 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 2247 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1880 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1859  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214
This theorem depends on definitions:  df-bi 198  df-or 866  df-ex 1860  df-nf 1864
This theorem is referenced by:  exlimih  2325  equs5aALT  2351  equs5eALT  2352  equsex  2459  nfeqf2OLD  2465  exdistrf  2495  equs5a  2506  equs5e  2507  mo2v  2639  moanim  2693  euan  2694  moexex  2705  2eu6  2722  ceqsex  3435  sbhypf  3447  vtoclgf  3457  vtoclg1f  3458  vtoclef  3474  rspn0  4135  reusv2lem1  5067  copsexg  5145  copsex2g  5147  ralxpf  5470  dmcoss  5586  fv3  6422  opabiota  6478  0neqopab  6924  zfregcl  8734  scottex  8991  scott0  8992  dfac5lem5  9229  zfcndpow  9719  zfcndreg  9720  zfcndinf  9721  reclem2pr  10151  mreiincl  16457  brabgaf  29741  cnvoprabOLD  29821  bnj607  31304  bnj900  31317  exisym1  32735  exlimii  33126  bj-exlimmpi  33209  bj-exlimmpbi  33210  bj-exlimmpbir  33211  dihglblem5  37073  eu2ndop1stv  41708
  Copyright terms: Public domain W3C validator