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

Theorem exlimi 2085
Description: Inference associated with 19.23 2079. See exlimiv 1857 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 2079 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1724 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1703  wnf 1707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-12 2046
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1704  df-nf 1709
This theorem is referenced by:  exlimih  2147  equs5aALT  2176  equs5eALT  2177  equsex  2291  nfeqf2  2296  exdistrf  2332  equs5a  2347  equs5e  2348  mo2v  2476  moanim  2528  euan  2529  moexex  2540  2eu6  2557  ceqsex  3239  sbhypf  3251  vtoclgf  3262  vtoclg1f  3263  vtoclef  3279  rspn0  3932  reusv2lem1  4866  copsexg  4954  copsex2g  4956  ralxpf  5266  dmcoss  5383  fv3  6204  tz6.12c  6211  opabiota  6259  0neqopab  6695  zfregcl  8496  zfregclOLD  8498  scottex  8745  scott0  8746  dfac5lem5  8947  zfcndpow  9435  zfcndreg  9436  zfcndinf  9437  reclem2pr  9867  mreiincl  16250  brabgaf  29404  cnvoprab  29483  bnj607  30971  bnj900  30984  exisym1  32407  exlimii  32802  bj-exlimmpi  32889  bj-exlimmpbi  32890  bj-exlimmpbir  32891  dihglblem5  36413  eu2ndop1stv  40971
  Copyright terms: Public domain W3C validator