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

Theorem exlimi 2216
 Description: Inference associated with 19.23 2210. See exlimiv 1931 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 2210 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimi.2 . 2 (𝜑𝜓)
42, 3mpgbi 1800 1 (∃𝑥𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1781  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2176 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786 This theorem is referenced by:  equs5av  2278  exlimih  2295  equs5aALT  2376  equs5eALT  2377  equsex  2432  exdistrf  2461  equs5a  2472  equs5e  2473  dfmoeu  2597  moanim  2685  euan  2686  moexexlem  2691  2eu6  2722  ceqsex  3491  sbhypf  3503  vtoclgf  3516  vtoclg1f  3517  vtoclef  3534  rspn0OLD  4270  reusv2lem1  5267  copsexgw  5349  copsexg  5350  copsex2g  5352  rexopabb  5383  0nelopab  5420  ralxpf  5685  dmcoss  5811  fv3  6667  opabiota  6725  oprabidw  7170  zfregcl  9046  scottex  9302  scott0  9303  dfac5lem5  9542  zfcndpow  10031  zfcndreg  10032  zfcndinf  10033  reclem2pr  10463  mreiincl  16863  brabgaf  30376  cnvoprabOLD  30486  bnj607  32302  bnj900  32315  exisym1  33886  exlimii  34270  bj-exlimmpi  34353  bj-exlimmpbi  34354  bj-exlimmpbir  34355  dihglblem5  38593  eu2ndop1stv  43678
 Copyright terms: Public domain W3C validator