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

Theorem exlimi 2210
Description: Inference associated with 19.23 2204. See exlimiv 1933 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 2204 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1801 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787
This theorem is referenced by:  sbalex  2235  equsexv  2260  equs5av  2271  exlimih  2286  equs5aALT  2364  equs5eALT  2365  equsex  2418  exdistrf  2447  equs5a  2457  equs5e  2458  dfmoeu  2536  moanim  2622  euan  2623  moexexlem  2628  2eu6  2658  ceqsex  3477  sbhypf  3490  vtoclgf  3502  vtoclg1f  3503  vtoclef  3522  rspn0OLD  4289  reusv2lem1  5323  copsexgw  5406  copsexg  5407  copsex2gOLD  5410  rexopabb  5443  0nelopabOLD  5483  ralxpf  5757  dmcoss  5882  fv3  6794  opabiota  6853  oprabidw  7308  zfregcl  9351  scottex  9641  scott0  9642  dfac5lem5  9881  zfcndpow  10370  zfcndreg  10371  zfcndinf  10372  reclem2pr  10802  mreiincl  17303  brabgaf  30945  cnvoprabOLD  31052  bnj607  32893  bnj900  32906  exisym1  34610  exlimii  35011  bj-exlimmpi  35094  bj-exlimmpbi  35095  bj-exlimmpbir  35096  dihglblem5  39309  eu2ndop1stv  44584  tworepnotupword  46488
  Copyright terms: Public domain W3C validator