Theorem reximdvai 2929

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.)

Hypothesis

Ref	Expression
reximdvai.1

Assertion

Ref	Expression
reximdvai

Distinct variable group:   ,

Proof of Theorem reximdvai

Step	Hyp	Ref	Expression
1		reximdvai.1	. . 3
2	1	ralrimiv 2869	. 2
3		rexim 2922	. 2
4	2, 3	syl 16	1

Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807  E.wrex 2808

This theorem is referenced by:  reximdv  2931  reximdva  2932  reuind  3303  wefrc  4878  isomin  6233  isofrlem  6236  onfununi  7031  oaordex  7226  odi  7247  omass  7248  omeulem1  7250  noinfep  8097  rankwflemb  8232  infxpenlem  8412  coflim  8662  coftr  8674  zorn2lem7  8903  suplem1pr  9451  axpre-sup  9567  climbdd  13494  filufint  20421  cvati  27285  atcvat4i  27316  mdsymlem2  27323  mdsymlem3  27324  sumdmdii  27334  iccllyscon  28695  dftrpred3g  29316  incsequz2  30242  upbdrech  31505  limcperiod  31634  cncfshift  31676  cncfperiod  31681  lcvat  34755  hlrelat3  35136  cvrval3  35137  cvrval4N  35138  2atlt  35163  cvrat4  35167  atbtwnexOLDN  35171  atbtwnex  35172  athgt  35180  2llnmat  35248  lnjatN  35504  2lnat  35508  cdlemb  35518  lhpexle3lem  35735  cdlemf1  36287  cdlemf2  36288  cdlemf  36289  cdlemk26b-3  36631  dvh4dimlem  37170

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813