Theorem r19.26 2984

Description: Restricted quantifier version of 19.26 1680. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.26

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		simpl 457	. . . 4
2	1	ralimi 2850	. . 3
3		simpr 461	. . . 4
4	3	ralimi 2850	. . 3
5	2, 4	jca 532	. 2
6		pm3.2 447	. . . 4
7	6	ral2imi 2845	. . 3
8	7	imp 429	. 2
9	5, 8	impbii 188	1

Syntax hints:  <->wb 184  /\wa 369  A.wral 2807

This theorem is referenced by:  r19.26-2  2985  r19.26-3  2986  ralbiim  2989  r19.27v  2990  r19.35  3004  reu8  3295  ssrab  3577  r19.28z  3921  r19.28zv  3924  r19.27z  3928  r19.27zv  3929  2ralunsn  4238  iuneq2  4347  disjxun  4450  asymref2  5389  cnvpo  5550  fncnv  5657  fnres  5702  fnopabg  5709  mpteqb  5970  eqfnfv3  5983  fvn0ssdmfun  6022  caoftrn  6575  iiner  7402  ixpeq2  7503  ixpin  7514  ixpfi2  7838  wemaplem2  7993  dfac5  8530  kmlem6  8556  eltsk2g  9150  intgru  9213  axgroth6  9227  fsequb  12085  rexanuz  13178  rexanre  13179  cau3lem  13187  rlimcn2  13413  o1of2  13435  o1rlimmul  13441  climbdd  13494  sqrt2irr  13982  gcdcllem1  14149  pc11  14403  prmreclem2  14435  catpropd  15104  issubc3  15218  fucinv  15342  ispos2  15577  issubg3  16219  issubg4  16220  pmtrdifwrdel2  16511  ringsrg  17237  cply1mul  18335  iunocv  18712  scmatf1  19033  cpmatsubgpmat  19221  tgval2  19457  1stcelcls  19962  ptclsg  20116  ptcnplem  20122  fbun  20341  txflf  20507  ucncn  20788  prdsmet  20873  metequiv  21012  metequiv2  21013  iscau4  21718  cmetcaulem  21727  evthicc2  21872  ismbfcn  22038  mbfi1flimlem  22129  rolle  22391  itgsubst  22450  plydivex  22693  ulmcaulem  22789  ulmcau  22790  ulmbdd  22793  ulmcn  22794  mumullem2  23454  2sqlem6  23644  axpasch  24244  axeuclid  24266  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  usg2wlkeq  24708  usgfiregdegfi  24911  usgreghash2spot  25069  frgrareg  25117  frgraregord013  25118  friendshipgt3  25121  rngoueqz  25432  ocsh  26201  spanuni  26462  riesz4i  26982  leopadd  27051  leoptri  27055  leoptr  27056  disjunsn  27453  mptfnf  27499  voliune  28201  volfiniune  28202  eulerpartlemr  28313  eulerpartlemn  28320  dfpo2  29184  poseq  29333  wfr3g  29342  wzel  29380  frr3g  29386  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnc  30069  neibastop1  30177  inixp  30219  intidl  30426  mzpincl  30666  lerabdioph  30738  ltrabdioph  30741  nerabdioph  30742  dvdsrabdioph  30743  dford3lem1  30968  stoweidlem7  31789  stoweidlem54  31836  dirkercncflem3  31887  2ralbiim  32179  2reu4a  32194  ralnralall  32294  ply1mulgsumlem1  32986  ldepsnlinclem1  33106  ldepsnlinclem2  33107  pclclN  35615  tendoeq2  36500

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-an 371  df-ral 2812