Theorem reximi 3068

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3054

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 3055

This theorem is referenced by:  r19.35  3088  r19.40  3096  2r19.29  3116  2reu2rex  3356  reu3  3684  2reu5  3715  reuan  3845  dfiun2g  4978  ssiun  4993  iinss  5003  elsnxp  6234  elunirn  7180  el2xpss  7964  iiner  8708  erovlem  8732  xpf1o  9047  enp1i  9158  unbnn2  9176  scott0  9771  dfac2b  10014  cflm  10133  alephsing  10159  numthcor  10377  zorng  10387  zornn0g  10388  ttukeyg  10400  uniimadom  10427  axgroth3  10714  qextlt  13094  qextle  13095  mptnn0fsuppd  13897  hashgt23el  14323  hash2sspr  14388  cshword  14690  rexanre  15246  climi2  15410  climi0  15411  rlimres  15457  lo1res  15458  caurcvgr  15573  caurcvg2  15577  caucvgb  15579  prodmolem2  15834  prodmo  15835  vdwnnlem1  16899  cshwsiun  17003  isnmnd  18638  efgrelexlemb  19655  nn0gsumfz0  19890  ablsimpgfind  20017  rhmdvdsr  20416  pmatcollpw2lem  22685  eltg2b  22867  neiptopuni  23038  neiptopnei  23040  ordtbas2  23099  lmcvg  23170  cnprest  23197  lmcnp  23212  nrmsep2  23264  bwth  23318  1stcfb  23353  islly2  23392  llycmpkgen  23460  txbas  23475  tx1stc  23558  cnextcn  23975  tmdcn2  23997  utoptop  24142  ucnima  24188  cfiluweak  24202  metrest  24432  metust  24466  cfilucfil  24467  metustbl  24474  xrhmeo  24864  cmetcaulem  25208  iundisj  25469  limcresi  25806  elply2  26121  aalioulem2  26261  ulmf  26311  lgamucov2  26969  2sqlem7  27355  2sqreultblem  27379  2sqreunnltblem  27382  pntrsumbnd  27497  nosupno  27635  nosupfv  27638  noinfno  27650  noinffv  27653  istrkg2ld  28431  tgisline  28598  umgr2edgneu  29185  umgr3v3e3cycl  30154  eucrctshift  30213  1to3vfriendship  30251  2pthfrgrrn  30252  grpoidval  30483  grporcan  30488  grpoinveu  30489  iunrnmptss  32535  iundisjf  32559  xlt2addrd  32732  xrofsup  32740  iundisjfi  32768  isdrng4  33251  tpr2rico  33915  esumc  34054  esumfsup  34073  esumpcvgval  34081  hasheuni  34088  esumiun  34097  voliune  34232  volfiniune  34233  dya2icoseg2  34281  dya2iocnei  34285  dya2iocuni  34286  omssubaddlem  34302  omssubadd  34303  afsval  34674  bnj31  34721  bnj1239  34807  bnj900  34931  bnj906  34932  bnj1398  35036  bnj1498  35063  nummin  35093  onvf1odlem1  35115  satfvsuclem1  35371  satfv1  35375  satfvsucsuc  35377  colinearex  36073  segcon2  36118  opnrebl2  36334  nlpfvineqsn  37422  fvineqsneq  37425  pibt2  37430  sdclem2  37761  heibor1lem  37828  grpomndo  37894  disjdmqsss  38819  disjdmqscossss  38820  dmqsblocks  38870  prtlem9  38882  prter1  38897  prter2  38899  hl2at  39423  cvrval4N  39432  athgt  39474  1dimN  39489  lhpexnle  40024  lhpexle1  40026  cdlemftr2  40584  cdlemftr1  40585  cdlemftr0  40586  cdlemg5  40623  cdlemg33c0  40720  mapdrvallem2  41663  sn-negex  42430  sn-negex2  42431  eldiophb  42769  rmxyelqirr  42922  hbtlem1  43135  hbtlem7  43137  ss2iundf  43671  mnupwd  44279  ismnushort  44313  iinssf  45154  founiiun  45195  founiiun0  45206  climuzlem  45760  stirlinglem13  46103  fourierdlem112  46235  2reuimp0  47124  2reuimp  47125  gbogbow  47766  sbgoldbo  47797  iineq0  48830  iuneqconst2  48833  iineqconst2  48834  sepcsepo  48937  seppsepf  48939