Theorem reximi 3081

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

Syntax hints:   → wi 4   ∈ wcel 2099  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-rex 3068

This theorem is referenced by:  r19.35  3105  r19.35OLD  3106  r19.29rOLD  3114  r19.40  3116  2r19.29  3136  r19.29d2rOLD  3138  r19.29vvaOLD  3211  2reu2rex  3387  reu3  3722  2reu5  3753  reuan  3889  dfiun2g  5033  ssiun  5049  iinss  5059  elsnxp  6295  elunirn  7261  el2xpss  8041  iiner  8808  erovlem  8832  xpf1o  9164  enp1i  9304  unbnn2  9325  scott0  9910  dfac2b  10154  cflm  10274  alephsing  10300  numthcor  10518  zorng  10528  zornn0g  10529  ttukeyg  10541  uniimadom  10568  axgroth3  10855  qextlt  13215  qextle  13216  mptnn0fsuppd  13996  hashgt23el  14416  hash2sspr  14482  cshword  14774  rexanre  15326  climi2  15488  climi0  15489  rlimres  15535  lo1res  15536  caurcvgr  15653  caurcvg2  15657  caucvgb  15659  prodmolem2  15912  prodmo  15913  vdwnnlem1  16964  cshwsiun  17069  isnmnd  18698  efgrelexlemb  19705  nn0gsumfz0  19940  ablsimpgfind  20067  rhmdvdsr  20447  pmatcollpw2lem  22692  eltg2b  22875  neiptopuni  23047  neiptopnei  23049  ordtbas2  23108  lmcvg  23179  cnprest  23206  lmcnp  23221  nrmsep2  23273  bwth  23327  1stcfb  23362  islly2  23401  llycmpkgen  23469  txbas  23484  tx1stc  23567  cnextcn  23984  tmdcn2  24006  utoptop  24152  ucnima  24199  cfiluweak  24213  metrest  24446  metust  24480  cfilucfil  24481  metustbl  24488  xrhmeo  24884  cmetcaulem  25229  iundisj  25490  limcresi  25827  elply2  26143  aalioulem2  26281  ulmf  26331  lgamucov2  26984  2sqlem7  27370  2sqreultblem  27394  2sqreunnltblem  27397  pntrsumbnd  27512  nosupno  27649  nosupfv  27652  noinfno  27664  noinffv  27667  istrkg2ld  28277  tgisline  28444  umgr2edgneu  29040  umgr3v3e3cycl  30007  eucrctshift  30066  1to3vfriendship  30104  2pthfrgrrn  30105  grpoidval  30336  grporcan  30341  grpoinveu  30342  iunrnmptss  32369  iundisjf  32392  xlt2addrd  32541  xrofsup  32550  iundisjfi  32577  isdrng4  32975  tpr2rico  33513  esumc  33670  esumfsup  33689  esumpcvgval  33697  hasheuni  33704  esumiun  33713  voliune  33848  volfiniune  33849  dya2icoseg2  33898  dya2iocnei  33902  dya2iocuni  33903  omssubaddlem  33919  omssubadd  33920  afsval  34303  bnj31  34350  bnj1239  34436  bnj900  34560  bnj906  34561  bnj1398  34665  bnj1498  34692  nummin  34714  satfvsuclem1  34969  satfv1  34973  satfvsucsuc  34975  colinearex  35656  segcon2  35701  opnrebl2  35805  nlpfvineqsn  36888  fvineqsneq  36891  pibt2  36896  sdclem2  37215  heibor1lem  37282  grpomndo  37348  disjdmqsss  38274  disjdmqscossss  38275  prtlem9  38336  prter1  38351  prter2  38353  hl2at  38878  cvrval4N  38887  athgt  38929  1dimN  38944  lhpexnle  39479  lhpexle1  39481  cdlemftr2  40039  cdlemftr1  40040  cdlemftr0  40041  cdlemg5  40078  cdlemg33c0  40175  mapdrvallem2  41118  sn-negex  41972  sn-negex2  41973  eldiophb  42177  rmxyelqirr  42330  rmxyelqirrOLD  42331  hbtlem1  42547  hbtlem7  42549  ss2iundf  43089  mnupwd  43704  ismnushort  43738  iinssf  44504  founiiun  44552  founiiun0  44563  climuzlem  45131  stirlinglem13  45474  fourierdlem112  45606  2reuimp0  46494  2reuimp  46495  gbogbow  47096  sbgoldbo  47127  sepcsepo  47945  seppsepf  47947