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

Theorem reximdai 2926
 Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
Hypotheses
Ref Expression
reximdai.1
reximdai.2
Assertion
Ref Expression
reximdai

Proof of Theorem reximdai
StepHypRef Expression
1 reximdai.1 . . 3
2 reximdai.2 . . 3
31, 2ralrimi 2857 . 2
4 rexim 2922 . 2
53, 4syl 16 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  F/wnf 1616  e.wcel 1818  A.wral 2807  E.wrex 2808 This theorem is referenced by:  reximdvaiOLD  2930  tz7.49  7129  hsmexlem2  8828  locfinreflem  27843  cmpcref  27853  indexdom  30225  filbcmb  30231  infrglb  31584  limsupre  31647  stoweidlem31  31813  stoweidlem34  31816  fourierdlem73  31962  2reurex  32186  cdlemefr29exN  36128 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-ral 2812  df-rex 2813
 Copyright terms: Public domain W3C validator