MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exim Unicode version

Theorem exim 1654
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
exim

Proof of Theorem exim
StepHypRef Expression
1 id 22 . 2
21aleximi 1653 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  E.wex 1612
This theorem is referenced by:  eximi  1656  aleximiOLD  1659  19.23v  1760  19.8a  1857  19.8aOLD  1858  19.9ht  1889  19.23t  1909  spimt  2005  elex2  3121  elex22  3122  vtoclegft  3181  spcimgft  3185  2exim  31284  pm11.71  31303  onfrALTlem2  33318  19.41rg  33323  ax6e2nd  33331  elex2VD  33638  elex22VD  33639  onfrALTlem2VD  33689  19.41rgVD  33702  ax6e2eqVD  33707  ax6e2ndVD  33708  ax6e2ndeqVD  33709  ax6e2ndALT  33730  ax6e2ndeqALT  33731  bj-axdd2  34180  bj-2exim  34203  bj-exlimh  34211  bj-alequex  34268  bj-spimtv  34278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator