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

Theorem exlimi 2217
Description: Inference associated with 19.23 2211. See exlimiv 1930 for a version with a disjoint variable 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 2211 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1798 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784
This theorem is referenced by:  sbalexOLD  2243  equsexv  2268  equs5av  2277  exlimih  2289  equs5aALT  2369  equs5eALT  2370  equsex  2423  exdistrf  2452  equs5a  2462  equs5e  2463  dfmoeu  2536  moanim  2620  euan  2621  moexexlem  2626  2eu6  2657  ceqsexOLD  3531  sbhypfOLD  3545  vtoclef  3563  vtoclgf  3569  vtoclg1f  3570  reusv2lem1  5398  copsexgw  5495  copsexg  5496  rexopabb  5533  ralxpf  5857  dmcoss  5985  fv3  6924  opabiota  6991  oprabidw  7462  zfregcl  9634  scottex  9925  scott0  9926  dfac5lem5  10167  zfcndpow  10656  zfcndreg  10657  zfcndinf  10658  reclem2pr  11088  mreiincl  17639  brabgaf  32620  bnj607  34930  bnj900  34943  exisym1  36425  exlimii  36832  bj-exlimmpi  36913  bj-exlimmpbi  36914  bj-exlimmpbir  36915  dihglblem5  41300  tworepnotupword  46901  eu2ndop1stv  47137  pgind  49236
  Copyright terms: Public domain W3C validator