Theorem reximi 3100

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

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
reximi	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	reximia 3097	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  r19.35  3120  r19.40  3128  2r19.29  3148  2reu2rex  3377  reu3  3684  2reu5  3715  reuan  3843  dfiun2g  4987  ssiun  5004  iinss  5014  elsnxp  6283  elunirn  7243  el2xpss  8031  iiner  8788  erovlem  8812  xpf1o  9136  enp1i  9248  unbnn2  9267  scott0b  9909  scott0OLD  9910  dfac2b  10181  cflm  10299  alephsing  10326  numthcor  10544  zorng  10554  zornn0g  10555  ttukeyg  10567  uniimadom  10600  axgroth3  10888  qextlt  13303  qextle  13304  mptnn0fsuppd  14110  hashgt23el  14537  hash2sspr  14602  cshword  14910  rexanre  15482  climi2  15646  climi0  15647  rlimres  15693  lo1res  15694  caurcvgr  15809  caurcvg2  15813  caucvgb  15815  prodmolem2  16070  prodmo  16071  vdwnnlem1  17135  cshwsiun  17239  isnmnd  18889  efgrelexlemb  19926  nn0gsumfz0  20161  ablsimpgfind  20288  rhmdvdsr  20720  isdrng4  20954  pmatcollpw2lem  23057  eltg2b  23239  neiptopuni  23410  neiptopnei  23412  ordtbas2  23471  lmcvg  23542  cnprest  23569  lmcnp  23584  nrmsep2  23636  bwth  23690  1stcfb  23725  islly2  23765  llycmpkgen  23833  txbas  23848  tx1stc  23931  cnextcn  24348  tmdcn2  24370  utoptop  24515  ucnima  24561  cfiluweak  24575  metrest  24805  metust  24839  cfilucfil  24840  metustbl  24847  xrhmeo  25229  cmetcaulem  25571  iundisj  25831  limcresi  26167  elply2  26476  aalioulem2  26624  ulmf  26673  lgamucov2  27330  2sqlem7  27715  2sqreultblem  27739  2sqreunnltblem  27742  pntrsumbnd  27857  nosupno  27994  nosupfv  27997  noinfno  28009  noinffv  28012  istrkg2ld  28856  tgisline  29029  cgrabasimass  29312  umgr2edgneu  29729  umgr3v3e3cycl  30719  eucrctshift  30778  1to3vfriendship  30816  2pthfrgrrn  30817  grpoidval  31049  grporcan  31054  grpoinveu  31055  iunrnmptss  33093  iundisjf  33117  xlt2addrd  33285  xrofsup  33293  iundisjfi  33322  dflringlem2  33961  tpr2rico  34478  esumc  34617  esumfsup  34636  esumpcvgval  34644  hasheuni  34651  esumiun  34660  voliune  34796  volfiniune  34797  dya2icoseg2  34845  dya2iocnei  34849  dya2iocuni  34850  omssubaddlem  34866  omssubadd  34867  afsval  35238  bnj31  35285  bnj1239  35370  bnj900  35494  bnj906  35495  bnj1398  35599  bnj1498  35626  nummin  35653  noinfepregs  35726  onvf1odlem1  35807  vonf1oonfo  35819  satfvsuclem1  36045  satfv1  36049  satfvsucsuc  36051  colinearex  36747  segcon2  36792  opnrebl2  37031  regsfromunir1  37250  nlpfvineqsn  38252  fvineqsneq  38255  pibt2  38260  negprop  38563  sdclem2  38596  heibor1lem  38663  grpomndo  38729  disjdmqsss  39757  disjdmqscossss  39758  dmqsblocks  39819  prtlem9  39841  prter1  39856  prter2  39858  hl2at  40382  cvrval4N  40391  athgt  40433  1dimN  40448  lhpexnle  40983  lhpexle1  40985  cdlemftr2  41543  cdlemftr1  41544  cdlemftr0  41545  cdlemg5  41582  cdlemg33c0  41679  mapdrvallem2  42622  sn-negex  43397  sn-negex2  43398  eldiophb  43706  rmxyelqirr  43855  hbtlem1  44068  hbtlem7  44070  ss2iundf  44603  mnupwd  45195  ismnushort  45229  iinssf  46074  founiiun  46115  founiiun0  46126  climuzlem  46675  stirlinglem13  47018  fourierdlem112  47150  2reuimp0  48106  2reuimp  48107  gbogbow  48776  sbgoldbo  48807  iineq0  49852  iuneqconst2  49855  iineqconst2  49856  sepcsepo  49957  seppsepf  49959