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

Theorem exlimi 2182
Description: Inference associated with 19.23 2176. See exlimiv 1908 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 2176 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1780 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1761  wnf 1765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-12 2141
This theorem depends on definitions:  df-bi 208  df-ex 1762  df-nf 1766
This theorem is referenced by:  exlimih  2263  equs5aALT  2341  equs5eALT  2342  equsex  2396  exdistrf  2426  equs5a  2437  equs5e  2438  dfmoeu  2572  moanim  2673  euan  2674  moexexlem  2681  2eu6  2714  ceqsex  3483  sbhypf  3495  vtoclgf  3508  vtoclg1f  3509  vtoclef  3526  rspn0  4233  reusv2lem1  5190  copsexg  5273  copsex2g  5275  rexopabb  5305  0nelopab  5340  ralxpf  5603  dmcoss  5723  fv3  6556  opabiota  6613  zfregcl  8904  scottex  9160  scott0  9161  dfac5lem5  9399  zfcndpow  9884  zfcndreg  9885  zfcndinf  9886  reclem2pr  10316  mreiincl  16696  brabgaf  30049  cnvoprabOLD  30144  bnj607  31804  bnj900  31817  exisym1  33381  exlimii  33724  bj-exlimmpi  33799  bj-exlimmpbi  33800  bj-exlimmpbir  33801  dihglblem5  37965  eu2ndop1stv  42840
  Copyright terms: Public domain W3C validator