Theorem reximi 3082

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  r19.35  3106  r19.35OLD  3107  r19.29rOLD  3115  r19.40  3117  2r19.29  3137  r19.29d2rOLD  3139  r19.29vvaOLD  3215  2reu2rex  3392  reu3  3736  2reu5  3767  reuan  3905  dfiun2g  5035  ssiun  5051  iinss  5061  elsnxp  6313  elunirn  7271  el2xpss  8061  iiner  8828  erovlem  8852  xpf1o  9178  enp1i  9311  unbnn2  9331  scott0  9924  dfac2b  10169  cflm  10288  alephsing  10314  numthcor  10532  zorng  10542  zornn0g  10543  ttukeyg  10555  uniimadom  10582  axgroth3  10869  qextlt  13242  qextle  13243  mptnn0fsuppd  14036  hashgt23el  14460  hash2sspr  14525  cshword  14826  rexanre  15382  climi2  15544  climi0  15545  rlimres  15591  lo1res  15592  caurcvgr  15707  caurcvg2  15711  caucvgb  15713  prodmolem2  15968  prodmo  15969  vdwnnlem1  17029  cshwsiun  17134  isnmnd  18764  efgrelexlemb  19783  nn0gsumfz0  20018  ablsimpgfind  20145  rhmdvdsr  20525  pmatcollpw2lem  22799  eltg2b  22982  neiptopuni  23154  neiptopnei  23156  ordtbas2  23215  lmcvg  23286  cnprest  23313  lmcnp  23328  nrmsep2  23380  bwth  23434  1stcfb  23469  islly2  23508  llycmpkgen  23576  txbas  23591  tx1stc  23674  cnextcn  24091  tmdcn2  24113  utoptop  24259  ucnima  24306  cfiluweak  24320  metrest  24553  metust  24587  cfilucfil  24588  metustbl  24595  xrhmeo  24991  cmetcaulem  25336  iundisj  25597  limcresi  25935  elply2  26250  aalioulem2  26390  ulmf  26440  lgamucov2  27097  2sqlem7  27483  2sqreultblem  27507  2sqreunnltblem  27510  pntrsumbnd  27625  nosupno  27763  nosupfv  27766  noinfno  27778  noinffv  27781  istrkg2ld  28483  tgisline  28650  umgr2edgneu  29246  umgr3v3e3cycl  30213  eucrctshift  30272  1to3vfriendship  30310  2pthfrgrrn  30311  grpoidval  30542  grporcan  30547  grpoinveu  30548  iunrnmptss  32586  iundisjf  32609  xlt2addrd  32769  xrofsup  32778  iundisjfi  32804  isdrng4  33279  tpr2rico  33873  esumc  34032  esumfsup  34051  esumpcvgval  34059  hasheuni  34066  esumiun  34075  voliune  34210  volfiniune  34211  dya2icoseg2  34260  dya2iocnei  34264  dya2iocuni  34265  omssubaddlem  34281  omssubadd  34282  afsval  34665  bnj31  34712  bnj1239  34798  bnj900  34922  bnj906  34923  bnj1398  35027  bnj1498  35054  nummin  35084  satfvsuclem1  35344  satfv1  35348  satfvsucsuc  35350  colinearex  36042  segcon2  36087  opnrebl2  36304  nlpfvineqsn  37392  fvineqsneq  37395  pibt2  37400  sdclem2  37729  heibor1lem  37796  grpomndo  37862  disjdmqsss  38784  disjdmqscossss  38785  prtlem9  38846  prter1  38861  prter2  38863  hl2at  39388  cvrval4N  39397  athgt  39439  1dimN  39454  lhpexnle  39989  lhpexle1  39991  cdlemftr2  40549  cdlemftr1  40550  cdlemftr0  40551  cdlemg5  40588  cdlemg33c0  40685  mapdrvallem2  41628  sn-negex  42424  sn-negex2  42425  eldiophb  42745  rmxyelqirr  42898  rmxyelqirrOLD  42899  hbtlem1  43112  hbtlem7  43114  ss2iundf  43649  mnupwd  44263  ismnushort  44297  iinssf  45078  founiiun  45122  founiiun0  45133  climuzlem  45699  stirlinglem13  46042  fourierdlem112  46174  2reuimp0  47064  2reuimp  47065  gbogbow  47681  sbgoldbo  47712  sepcsepo  48723  seppsepf  48725