Theorem reximi 2925

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1

Assertion

Ref	Expression
reximi

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3
2	1	a1i 11	. 2
3	2	reximia 2923	1

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

This theorem is referenced by:  r19.29d2r  3000  r19.40  3008  reu3  3289  2reu5  3308  ssiun  4372  iinss  4381  elunirn  6163  iiner  7402  erovlem  7426  xpf1o  7699  unbnn2  7797  scott0  8325  dfac2  8532  cflm  8651  alephsing  8677  numthcor  8895  zorng  8905  zornn0g  8906  ttukeyg  8918  uniimadom  8940  axgroth3  9230  qextlt  11431  qextle  11432  mptnn0fsuppd  12104  cshword  12762  rexanre  13179  climi2  13334  climi0  13335  rlimres  13381  lo1res  13382  caurcvgr  13496  caurcvg2  13500  caucvgb  13502  prodmolem2  13742  prodmo  13743  vdwnnlem1  14513  cshwsiun  14584  isnmnd  15924  efgrelexlemb  16768  nn0gsumfz0  17013  pmatcollpw2lem  19278  eltg2b  19460  neiptopuni  19631  neiptopnei  19633  ordtbas2  19692  lmcvg  19763  cnprest  19790  lmcnp  19805  nrmsep2  19857  bwth  19910  1stcfb  19946  islly2  19985  llycmpkgen  20053  txbas  20068  tx1stc  20151  cnextcn  20567  tmdcn2  20588  utoptop  20737  ucnima  20784  cfiluweak  20798  metrest  21027  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  metustblOLD  21083  metustbl  21084  xrhmeo  21446  cmetcaulem  21727  iundisj  21958  limcresi  22289  elply2  22593  aalioulem2  22729  ulmf  22777  2sqlem7  23645  pntrsumbnd  23751  istrkg2ld  23858  tgisline  24007  usgra2edg1  24383  3v3e3cycl1  24644  wwlkn0  24689  1to3vfriendship  25008  2pthfrgrarn  25009  grpoidval  25218  grporcan  25223  grpoinveu  25224  grpomndo  25348  iundisjf  27448  xlt2addrd  27578  xrge0infss  27580  xrofsup  27582  iundisjfi  27601  rhmdvdsr  27808  tpr2rico  27894  esumc  28062  esumfsup  28076  esumpcvgval  28084  hasheuni  28091  voliune  28201  volfiniune  28202  dya2icoseg2  28249  dya2iocnei  28253  dya2iocuni  28254  afsval  28551  lgamucov2  28581  colinearex  29710  segcon2  29755  opnrebl2  30139  sdclem2  30235  heibor1lem  30305  2r19.29  30595  prtlem9  30605  prtlem11  30607  prter1  30620  prter2  30622  eldiophb  30690  rmxyelqirr  30846  hbtlem1  31072  hbtlem7  31074  stirlinglem13  31868  fourierdlem112  32001  reuan  32185  2reu2rex  32188  usg2edgneu  32412  bnj31  33772  bnj1239  33864  bnj900  33987  bnj906  33988  bnj1398  34090  bnj1498  34117  hl2at  35129  cvrval4N  35138  athgt  35180  1dimN  35195  lhpexnle  35730  lhpexle1  35732  cdlemftr2  36292  cdlemftr1  36293  cdlemftr0  36294  cdlemg5  36331  cdlemg33c0  36428  mapdrvallem2  37372

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-ex 1613  df-ral 2812  df-rex 2813