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

Theorem exlimi 2084
Description: Inference associated with 19.23 2078. See exlimiv 1855 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 2078 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1722 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707
This theorem is referenced by:  exlimih  2144  equs5aALT  2176  equs5eALT  2177  equsex  2292  nfeqf2  2296  exdistrf  2332  equs5a  2347  equs5e  2348  mo2v  2476  moanim  2528  euan  2529  moexex  2540  2eu6  2557  ceqsex  3231  sbhypf  3243  vtoclgf  3254  vtoclg1f  3255  vtoclef  3271  rspn0  3916  reusv2lem1  4838  copsexg  4926  copsex2g  4928  ralxpf  5238  dmcoss  5355  fv3  6173  tz6.12c  6180  opabiota  6228  0neqopab  6663  zfregcl  8459  zfregclOLD  8461  scottex  8708  scott0  8709  dfac5lem5  8910  zfcndpow  9398  zfcndreg  9399  zfcndinf  9400  reclem2pr  9830  mreiincl  16196  brabgaf  29304  cnvoprab  29382  bnj607  30747  bnj900  30760  exisym1  32118  exlimii  32514  bj-exlimmpi  32605  bj-exlimmpbi  32606  bj-exlimmpbir  32607  dihglblem5  36106  eu2ndop1stv  40536
  Copyright terms: Public domain W3C validator