Theorem reximi 3083

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3070

This theorem is referenced by:  r19.35  3107  r19.35OLD  3108  r19.29rOLD  3116  r19.40  3118  2r19.29  3138  r19.29d2rOLD  3140  r19.29vvaOLD  3216  2reu2rex  3393  reu3  3732  2reu5  3763  reuan  3895  dfiun2g  5029  ssiun  5045  iinss  5055  elsnxp  6310  elunirn  7272  el2xpss  8063  iiner  8830  erovlem  8854  xpf1o  9180  enp1i  9314  unbnn2  9334  scott0  9927  dfac2b  10172  cflm  10291  alephsing  10317  numthcor  10535  zorng  10545  zornn0g  10546  ttukeyg  10558  uniimadom  10585  axgroth3  10872  qextlt  13246  qextle  13247  mptnn0fsuppd  14040  hashgt23el  14464  hash2sspr  14529  cshword  14830  rexanre  15386  climi2  15548  climi0  15549  rlimres  15595  lo1res  15596  caurcvgr  15711  caurcvg2  15715  caucvgb  15717  prodmolem2  15972  prodmo  15973  vdwnnlem1  17034  cshwsiun  17138  isnmnd  18752  efgrelexlemb  19769  nn0gsumfz0  20004  ablsimpgfind  20131  rhmdvdsr  20509  pmatcollpw2lem  22784  eltg2b  22967  neiptopuni  23139  neiptopnei  23141  ordtbas2  23200  lmcvg  23271  cnprest  23298  lmcnp  23313  nrmsep2  23365  bwth  23419  1stcfb  23454  islly2  23493  llycmpkgen  23561  txbas  23576  tx1stc  23659  cnextcn  24076  tmdcn2  24098  utoptop  24244  ucnima  24291  cfiluweak  24305  metrest  24538  metust  24572  cfilucfil  24573  metustbl  24580  xrhmeo  24978  cmetcaulem  25323  iundisj  25584  limcresi  25921  elply2  26236  aalioulem2  26376  ulmf  26426  lgamucov2  27083  2sqlem7  27469  2sqreultblem  27493  2sqreunnltblem  27496  pntrsumbnd  27611  nosupno  27749  nosupfv  27752  noinfno  27764  noinffv  27767  istrkg2ld  28469  tgisline  28636  umgr2edgneu  29232  umgr3v3e3cycl  30204  eucrctshift  30263  1to3vfriendship  30301  2pthfrgrrn  30302  grpoidval  30533  grporcan  30538  grpoinveu  30539  iunrnmptss  32579  iundisjf  32603  xlt2addrd  32763  xrofsup  32772  iundisjfi  32799  isdrng4  33299  tpr2rico  33912  esumc  34053  esumfsup  34072  esumpcvgval  34080  hasheuni  34087  esumiun  34096  voliune  34231  volfiniune  34232  dya2icoseg2  34281  dya2iocnei  34285  dya2iocuni  34286  omssubaddlem  34302  omssubadd  34303  afsval  34687  bnj31  34734  bnj1239  34820  bnj900  34944  bnj906  34945  bnj1398  35049  bnj1498  35076  nummin  35106  satfvsuclem1  35365  satfv1  35369  satfvsucsuc  35371  colinearex  36062  segcon2  36107  opnrebl2  36323  nlpfvineqsn  37411  fvineqsneq  37414  pibt2  37419  sdclem2  37750  heibor1lem  37817  grpomndo  37883  disjdmqsss  38804  disjdmqscossss  38805  prtlem9  38866  prter1  38881  prter2  38883  hl2at  39408  cvrval4N  39417  athgt  39459  1dimN  39474  lhpexnle  40009  lhpexle1  40011  cdlemftr2  40569  cdlemftr1  40570  cdlemftr0  40571  cdlemg5  40608  cdlemg33c0  40705  mapdrvallem2  41648  sn-negex  42452  sn-negex2  42453  eldiophb  42773  rmxyelqirr  42926  rmxyelqirrOLD  42927  hbtlem1  43140  hbtlem7  43142  ss2iundf  43677  mnupwd  44291  ismnushort  44325  iinssf  45148  founiiun  45189  founiiun0  45200  climuzlem  45763  stirlinglem13  46106  fourierdlem112  46238  2reuimp0  47131  2reuimp  47132  gbogbow  47748  sbgoldbo  47779  sepcsepo  48831  seppsepf  48833