Theorem reximi 3076

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

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 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.35  3096  r19.40  3104  2r19.29  3124  2reu2rex  3364  reu3  3687  2reu5  3718  reuan  3848  dfiun2g  4987  ssiun  5004  iinss  5014  elsnxp  6257  elunirn  7207  el2xpss  7991  iiner  8738  erovlem  8762  xpf1o  9079  enp1i  9191  unbnn2  9209  scott0  9810  dfac2b  10053  cflm  10172  alephsing  10198  numthcor  10416  zorng  10426  zornn0g  10427  ttukeyg  10439  uniimadom  10466  axgroth3  10754  qextlt  13130  qextle  13131  mptnn0fsuppd  13933  hashgt23el  14359  hash2sspr  14424  cshword  14726  rexanre  15282  climi2  15446  climi0  15447  rlimres  15493  lo1res  15494  caurcvgr  15609  caurcvg2  15613  caucvgb  15615  prodmolem2  15870  prodmo  15871  vdwnnlem1  16935  cshwsiun  17039  isnmnd  18675  efgrelexlemb  19691  nn0gsumfz0  19926  ablsimpgfind  20053  rhmdvdsr  20453  pmatcollpw2lem  22733  eltg2b  22915  neiptopuni  23086  neiptopnei  23088  ordtbas2  23147  lmcvg  23218  cnprest  23245  lmcnp  23260  nrmsep2  23312  bwth  23366  1stcfb  23401  islly2  23440  llycmpkgen  23508  txbas  23523  tx1stc  23606  cnextcn  24023  tmdcn2  24045  utoptop  24190  ucnima  24236  cfiluweak  24250  metrest  24480  metust  24514  cfilucfil  24515  metustbl  24522  xrhmeo  24912  cmetcaulem  25256  iundisj  25517  limcresi  25854  elply2  26169  aalioulem2  26309  ulmf  26359  lgamucov2  27017  2sqlem7  27403  2sqreultblem  27427  2sqreunnltblem  27430  pntrsumbnd  27545  nosupno  27683  nosupfv  27686  noinfno  27698  noinffv  27701  istrkg2ld  28544  tgisline  28711  umgr2edgneu  29299  umgr3v3e3cycl  30271  eucrctshift  30330  1to3vfriendship  30368  2pthfrgrrn  30369  grpoidval  30600  grporcan  30605  grpoinveu  30606  iunrnmptss  32651  iundisjf  32675  xlt2addrd  32849  xrofsup  32857  iundisjfi  32886  isdrng4  33388  tpr2rico  34089  esumc  34228  esumfsup  34247  esumpcvgval  34255  hasheuni  34262  esumiun  34271  voliune  34406  volfiniune  34407  dya2icoseg2  34455  dya2iocnei  34459  dya2iocuni  34460  omssubaddlem  34476  omssubadd  34477  afsval  34848  bnj31  34895  bnj1239  34980  bnj900  35104  bnj906  35105  bnj1398  35209  bnj1498  35236  nummin  35268  r1omhf  35281  noinfepregs  35308  onvf1odlem1  35316  satfvsuclem1  35572  satfv1  35576  satfvsucsuc  35578  colinearex  36273  segcon2  36318  opnrebl2  36534  regsfromunir1  36689  nlpfvineqsn  37653  fvineqsneq  37656  pibt2  37661  sdclem2  37982  heibor1lem  38049  grpomndo  38115  disjdmqsss  39145  disjdmqscossss  39146  dmqsblocks  39207  prtlem9  39229  prter1  39244  prter2  39246  hl2at  39770  cvrval4N  39779  athgt  39821  1dimN  39836  lhpexnle  40371  lhpexle1  40373  cdlemftr2  40931  cdlemftr1  40932  cdlemftr0  40933  cdlemg5  40970  cdlemg33c0  41067  mapdrvallem2  42010  sn-negex  42777  sn-negex2  42778  eldiophb  43103  rmxyelqirr  43256  hbtlem1  43469  hbtlem7  43471  ss2iundf  44004  mnupwd  44612  ismnushort  44646  iinssf  45486  founiiun  45527  founiiun0  45538  climuzlem  46090  stirlinglem13  46433  fourierdlem112  46565  2reuimp0  47463  2reuimp  47464  gbogbow  48105  sbgoldbo  48136  iineq0  49168  iuneqconst2  49171  iineqconst2  49172  sepcsepo  49275  seppsepf  49277