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 2106  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  r19.35  3107  r19.35OLD  3108  r19.29rOLD  3116  r19.40  3118  2r19.29  3132  r19.29d2rOLD  3134  r19.29vvaOLD  3204  2reu2rex  3365  reu3  3688  2reu5  3719  reuan  3855  dfiun2g  4995  ssiun  5011  iinss  5021  elsnxp  6248  elunirn  7203  el2xpss  7974  iiner  8735  erovlem  8759  xpf1o  9090  enp1i  9230  unbnn2  9251  scott0  9831  dfac2b  10075  cflm  10195  alephsing  10221  numthcor  10439  zorng  10449  zornn0g  10450  ttukeyg  10462  uniimadom  10489  axgroth3  10776  qextlt  13132  qextle  13133  mptnn0fsuppd  13913  hashgt23el  14334  hash2sspr  14399  cshword  14691  rexanre  15243  climi2  15405  climi0  15406  rlimres  15452  lo1res  15453  caurcvgr  15570  caurcvg2  15574  caucvgb  15576  prodmolem2  15829  prodmo  15830  vdwnnlem1  16878  cshwsiun  16983  isnmnd  18574  efgrelexlemb  19546  nn0gsumfz0  19776  ablsimpgfind  19903  rhmdvdsr  20197  pmatcollpw2lem  22163  eltg2b  22346  neiptopuni  22518  neiptopnei  22520  ordtbas2  22579  lmcvg  22650  cnprest  22677  lmcnp  22692  nrmsep2  22744  bwth  22798  1stcfb  22833  islly2  22872  llycmpkgen  22940  txbas  22955  tx1stc  23038  cnextcn  23455  tmdcn2  23477  utoptop  23623  ucnima  23670  cfiluweak  23684  metrest  23917  metust  23951  cfilucfil  23952  metustbl  23959  xrhmeo  24346  cmetcaulem  24689  iundisj  24949  limcresi  25286  elply2  25594  aalioulem2  25730  ulmf  25778  lgamucov2  26425  2sqlem7  26809  2sqreultblem  26833  2sqreunnltblem  26836  pntrsumbnd  26951  nosupno  27088  nosupfv  27091  noinfno  27103  noinffv  27106  istrkg2ld  27465  tgisline  27632  umgr2edgneu  28225  umgr3v3e3cycl  29191  eucrctshift  29250  1to3vfriendship  29288  2pthfrgrrn  29289  grpoidval  29518  grporcan  29523  grpoinveu  29524  iunrnmptss  31551  iundisjf  31574  xlt2addrd  31731  xrofsup  31740  iundisjfi  31767  tpr2rico  32582  esumc  32739  esumfsup  32758  esumpcvgval  32766  hasheuni  32773  esumiun  32782  voliune  32917  volfiniune  32918  dya2icoseg2  32967  dya2iocnei  32971  dya2iocuni  32972  omssubaddlem  32988  omssubadd  32989  afsval  33373  bnj31  33420  bnj1239  33506  bnj900  33630  bnj906  33631  bnj1398  33735  bnj1498  33762  nummin  33784  satfvsuclem1  34040  satfv1  34044  satfvsucsuc  34046  colinearex  34721  segcon2  34766  opnrebl2  34869  nlpfvineqsn  35953  fvineqsneq  35956  pibt2  35961  sdclem2  36274  heibor1lem  36341  grpomndo  36407  disjdmqsss  37337  disjdmqscossss  37338  prtlem9  37399  prter1  37414  prter2  37416  hl2at  37941  cvrval4N  37950  athgt  37992  1dimN  38007  lhpexnle  38542  lhpexle1  38544  cdlemftr2  39102  cdlemftr1  39103  cdlemftr0  39104  cdlemg5  39141  cdlemg33c0  39238  mapdrvallem2  40181  sn-negex  40944  sn-negex2  40945  eldiophb  41138  rmxyelqirr  41291  rmxyelqirrOLD  41292  hbtlem1  41508  hbtlem7  41510  ss2iundf  42053  mnupwd  42669  ismnushort  42703  iinssf  43470  founiiun  43518  founiiun0  43531  climuzlem  44104  stirlinglem13  44447  fourierdlem112  44579  2reuimp0  45466  2reuimp  45467  gbogbow  46068  sbgoldbo  46099  sepcsepo  47079  seppsepf  47081