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

Theorem exlimi 2205
Description: Inference associated with 19.23 2199. See exlimiv 1925 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 2199 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1792 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778
This theorem is referenced by:  sbalex  2230  equsexv  2254  equs5av  2265  exlimih  2278  equs5aALT  2357  equs5eALT  2358  equsex  2411  exdistrf  2440  equs5a  2450  equs5e  2451  dfmoeu  2524  moanim  2608  euan  2609  moexexlem  2614  2eu6  2645  ceqsexOLD  3513  sbhypfOLD  3529  vtoclef  3541  vtoclgf  3548  vtoclg1f  3549  rspn0OLD  4353  reusv2lem1  5398  copsexgw  5492  copsexg  5493  copsex2gOLD  5496  rexopabb  5530  0nelopabOLD  5570  ralxpf  5849  dmcoss  5974  fv3  6914  opabiota  6980  oprabidw  7450  zfregcl  9619  scottex  9910  scott0  9911  dfac5lem5  10152  zfcndpow  10641  zfcndreg  10642  zfcndinf  10643  reclem2pr  11073  mreiincl  17579  brabgaf  32477  cnvoprabOLD  32584  bnj607  34678  bnj900  34691  exisym1  36039  exlimii  36439  bj-exlimmpi  36521  bj-exlimmpbi  36522  bj-exlimmpbir  36523  dihglblem5  40901  tworepnotupword  46410  eu2ndop1stv  46643  pgind  48334
  Copyright terms: Public domain W3C validator