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

Step	Hyp	Ref	Expression
1		reximdai.1	. . 3
2		reximdai.2	. . 3
3	1, 2	ralrimi 2857	. 2
4		rexim 2922	. 2
5	3, 4	syl 16	1

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