Theorem reximi 3094

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

Syntax hints:   → wi 4   ∈ wcel 2136  ∃wrex 3080

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-rex 3081

This theorem is referenced by:  r19.35  3114  r19.40  3122  2r19.29  3142  2reu2rex  3373  reu3  3684  2reu5  3715  reuan  3844  dfiun2g  4981  ssiun  4998  iinss  5008  elsnxp  6267  elunirn  7224  el2xpss  8007  iiner  8759  erovlem  8783  xpf1o  9100  enp1i  9212  unbnn2  9230  scott0  9834  dfac2b  10077  cflm  10196  alephsing  10223  numthcor  10441  zorng  10451  zornn0g  10452  ttukeyg  10464  uniimadom  10491  axgroth3  10779  qextlt  13196  qextle  13197  mptnn0fsuppd  14001  hashgt23el  14427  hash2sspr  14492  cshword  14794  rexanre  15350  climi2  15514  climi0  15515  rlimres  15561  lo1res  15562  caurcvgr  15677  caurcvg2  15681  caucvgb  15683  prodmolem2  15941  prodmo  15942  vdwnnlem1  17007  cshwsiun  17111  isnmnd  18748  efgrelexlemb  19766  nn0gsumfz0  20001  ablsimpgfind  20128  rhmdvdsr  20530  pmatcollpw2lem  22810  eltg2b  22992  neiptopuni  23163  neiptopnei  23165  ordtbas2  23224  lmcvg  23295  cnprest  23322  lmcnp  23337  nrmsep2  23389  bwth  23443  1stcfb  23478  islly2  23517  llycmpkgen  23585  txbas  23600  tx1stc  23683  cnextcn  24100  tmdcn2  24122  utoptop  24267  ucnima  24313  cfiluweak  24327  metrest  24557  metust  24591  cfilucfil  24592  metustbl  24599  xrhmeo  24981  cmetcaulem  25323  iundisj  25583  limcresi  25920  elply2  26229  aalioulem2  26367  ulmf  26415  lgamucov2  27073  2sqlem7  27458  2sqreultblem  27482  2sqreunnltblem  27485  pntrsumbnd  27600  nosupno  27737  nosupfv  27740  noinfno  27752  noinffv  27755  istrkg2ld  28599  tgisline  28766  umgr2edgneu  29354  umgr3v3e3cycl  30325  eucrctshift  30384  1to3vfriendship  30422  2pthfrgrrn  30423  grpoidval  30655  grporcan  30660  grpoinveu  30661  iunrnmptss  32707  iundisjf  32731  xlt2addrd  32904  xrofsup  32912  iundisjfi  32941  isdrng4  33436  dflringlem2  33645  tpr2rico  34163  esumc  34302  esumfsup  34321  esumpcvgval  34329  hasheuni  34336  esumiun  34345  voliune  34480  volfiniune  34481  dya2icoseg2  34529  dya2iocnei  34533  dya2iocuni  34534  omssubaddlem  34550  omssubadd  34551  afsval  34925  bnj31  34972  bnj1239  35057  bnj900  35181  bnj906  35182  bnj1398  35286  bnj1498  35313  nummin  35344  r1omhf  35357  noinfepregs  35384  onvf1odlem1  35401  satfvsuclem1  35657  satfv1  35661  satfvsucsuc  35663  colinearex  36358  segcon2  36403  opnrebl2  36629  regsfromunir1  36848  nlpfvineqsn  37851  fvineqsneq  37854  pibt2  37859  sdclem2  38189  heibor1lem  38256  grpomndo  38322  disjdmqsss  39352  disjdmqscossss  39353  dmqsblocks  39414  prtlem9  39436  prter1  39451  prter2  39453  hl2at  39977  cvrval4N  39986  athgt  40028  1dimN  40043  lhpexnle  40578  lhpexle1  40580  cdlemftr2  41138  cdlemftr1  41139  cdlemftr0  41140  cdlemg5  41177  cdlemg33c0  41274  mapdrvallem2  42217  sn-negex  42975  sn-negex2  42976  eldiophb  43286  rmxyelqirr  43435  hbtlem1  43648  hbtlem7  43650  ss2iundf  44183  mnupwd  44791  ismnushort  44825  iinssf  45664  founiiun  45705  founiiun0  45716  climuzlem  46265  stirlinglem13  46608  fourierdlem112  46740  2reuimp0  47656  2reuimp  47657  gbogbow  48326  sbgoldbo  48357  iineq0  49389  iuneqconst2  49392  iineqconst2  49393  sepcsepo  49496  seppsepf  49498