Theorem reximi 3072

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 3069	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  r19.35  3092  r19.40  3100  2r19.29  3120  2reu2rex  3360  reu3  3683  2reu5  3714  reuan  3844  dfiun2g  4982  ssiun  4999  iinss  5009  elsnxp  6246  elunirn  7194  el2xpss  7978  iiner  8722  erovlem  8746  xpf1o  9062  enp1i  9173  unbnn2  9191  scott0  9789  dfac2b  10032  cflm  10151  alephsing  10177  numthcor  10395  zorng  10405  zornn0g  10406  ttukeyg  10418  uniimadom  10445  axgroth3  10732  qextlt  13112  qextle  13113  mptnn0fsuppd  13915  hashgt23el  14341  hash2sspr  14406  cshword  14708  rexanre  15264  climi2  15428  climi0  15429  rlimres  15475  lo1res  15476  caurcvgr  15591  caurcvg2  15595  caucvgb  15597  prodmolem2  15852  prodmo  15853  vdwnnlem1  16917  cshwsiun  17021  isnmnd  18656  efgrelexlemb  19672  nn0gsumfz0  19907  ablsimpgfind  20034  rhmdvdsr  20433  pmatcollpw2lem  22702  eltg2b  22884  neiptopuni  23055  neiptopnei  23057  ordtbas2  23116  lmcvg  23187  cnprest  23214  lmcnp  23229  nrmsep2  23281  bwth  23335  1stcfb  23370  islly2  23409  llycmpkgen  23477  txbas  23492  tx1stc  23575  cnextcn  23992  tmdcn2  24014  utoptop  24159  ucnima  24205  cfiluweak  24219  metrest  24449  metust  24483  cfilucfil  24484  metustbl  24491  xrhmeo  24881  cmetcaulem  25225  iundisj  25486  limcresi  25823  elply2  26138  aalioulem2  26278  ulmf  26328  lgamucov2  26986  2sqlem7  27372  2sqreultblem  27396  2sqreunnltblem  27399  pntrsumbnd  27514  nosupno  27652  nosupfv  27655  noinfno  27667  noinffv  27670  istrkg2ld  28448  tgisline  28615  umgr2edgneu  29203  umgr3v3e3cycl  30175  eucrctshift  30234  1to3vfriendship  30272  2pthfrgrrn  30273  grpoidval  30504  grporcan  30509  grpoinveu  30510  iunrnmptss  32556  iundisjf  32580  xlt2addrd  32753  xrofsup  32761  iundisjfi  32789  isdrng4  33272  tpr2rico  33936  esumc  34075  esumfsup  34094  esumpcvgval  34102  hasheuni  34109  esumiun  34118  voliune  34253  volfiniune  34254  dya2icoseg2  34302  dya2iocnei  34306  dya2iocuni  34307  omssubaddlem  34323  omssubadd  34324  afsval  34695  bnj31  34742  bnj1239  34828  bnj900  34952  bnj906  34953  bnj1398  35057  bnj1498  35084  nummin  35115  r1omhf  35128  onvf1odlem1  35158  satfvsuclem1  35414  satfv1  35418  satfvsucsuc  35420  colinearex  36115  segcon2  36160  opnrebl2  36376  nlpfvineqsn  37464  fvineqsneq  37467  pibt2  37472  sdclem2  37792  heibor1lem  37859  grpomndo  37925  disjdmqsss  38910  disjdmqscossss  38911  dmqsblocks  38961  prtlem9  38973  prter1  38988  prter2  38990  hl2at  39514  cvrval4N  39523  athgt  39565  1dimN  39580  lhpexnle  40115  lhpexle1  40117  cdlemftr2  40675  cdlemftr1  40676  cdlemftr0  40677  cdlemg5  40714  cdlemg33c0  40811  mapdrvallem2  41754  sn-negex  42526  sn-negex2  42527  eldiophb  42864  rmxyelqirr  43017  hbtlem1  43230  hbtlem7  43232  ss2iundf  43766  mnupwd  44374  ismnushort  44408  iinssf  45249  founiiun  45290  founiiun0  45301  climuzlem  45855  stirlinglem13  46198  fourierdlem112  46330  2reuimp0  47228  2reuimp  47229  gbogbow  47870  sbgoldbo  47901  iineq0  48934  iuneqconst2  48937  iineqconst2  48938  sepcsepo  49041  seppsepf  49043