Theorem reximi 3103

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

Syntax hints:   → wi 4   ∈ wcel 2145  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  r19.35  3123  r19.40  3131  2r19.29  3151  2reu2rex  3382  reu3  3693  2reu5  3724  reuan  3852  dfiun2g  4990  ssiun  5007  iinss  5017  elsnxp  6282  elunirn  7239  el2xpss  8022  iiner  8775  erovlem  8799  xpf1o  9115  enp1i  9227  unbnn2  9245  scott0  9848  dfac2b  10102  cflm  10221  alephsing  10248  numthcor  10466  zorng  10476  zornn0g  10477  ttukeyg  10489  uniimadom  10516  axgroth3  10804  qextlt  13220  qextle  13221  mptnn0fsuppd  14025  hashgt23el  14451  hash2sspr  14516  cshword  14818  rexanre  15388  climi2  15552  climi0  15553  rlimres  15599  lo1res  15600  caurcvgr  15715  caurcvg2  15719  caucvgb  15721  prodmolem2  15979  prodmo  15980  vdwnnlem1  17045  cshwsiun  17149  isnmnd  18786  efgrelexlemb  19811  nn0gsumfz0  20046  ablsimpgfind  20173  rhmdvdsr  20582  pmatcollpw2lem  22895  eltg2b  23077  neiptopuni  23248  neiptopnei  23250  ordtbas2  23309  lmcvg  23380  cnprest  23407  lmcnp  23422  nrmsep2  23474  bwth  23528  1stcfb  23563  islly2  23602  llycmpkgen  23670  txbas  23685  tx1stc  23768  cnextcn  24185  tmdcn2  24207  utoptop  24352  ucnima  24398  cfiluweak  24412  metrest  24642  metust  24676  cfilucfil  24677  metustbl  24684  xrhmeo  25066  cmetcaulem  25408  iundisj  25668  limcresi  26005  elply2  26314  aalioulem2  26455  ulmf  26503  lgamucov2  27161  2sqlem7  27546  2sqreultblem  27570  2sqreunnltblem  27573  pntrsumbnd  27688  nosupno  27825  nosupfv  27828  noinfno  27840  noinffv  27843  istrkg2ld  28687  tgisline  28854  umgr2edgneu  29473  umgr3v3e3cycl  30444  eucrctshift  30503  1to3vfriendship  30541  2pthfrgrrn  30542  grpoidval  30774  grporcan  30779  grpoinveu  30780  iunrnmptss  32820  iundisjf  32844  xlt2addrd  33016  xrofsup  33024  iundisjfi  33053  isdrng4  33531  dflringlem2  33702  tpr2rico  34219  esumc  34358  esumfsup  34377  esumpcvgval  34385  hasheuni  34392  esumiun  34401  voliune  34536  volfiniune  34537  dya2icoseg2  34585  dya2iocnei  34589  dya2iocuni  34590  omssubaddlem  34606  omssubadd  34607  afsval  34978  bnj31  35025  bnj1239  35110  bnj900  35234  bnj906  35235  bnj1398  35339  bnj1498  35366  nummin  35399  r1omhf  35414  noinfepregs  35441  onvf1odlem1  35458  vonf1oonfo  35470  satfvsuclem1  35722  satfv1  35726  satfvsucsuc  35728  colinearex  36423  segcon2  36468  opnrebl2  36694  regsfromunir1  36913  nlpfvineqsn  37915  fvineqsneq  37918  pibt2  37923  sdclem2  38253  heibor1lem  38320  grpomndo  38386  disjdmqsss  39416  disjdmqscossss  39417  dmqsblocks  39478  prtlem9  39500  prter1  39515  prter2  39517  hl2at  40041  cvrval4N  40050  athgt  40092  1dimN  40107  lhpexnle  40642  lhpexle1  40644  cdlemftr2  41202  cdlemftr1  41203  cdlemftr0  41204  cdlemg5  41241  cdlemg33c0  41338  mapdrvallem2  42281  sn-negex  43039  sn-negex2  43040  eldiophb  43350  rmxyelqirr  43499  hbtlem1  43712  hbtlem7  43714  ss2iundf  44247  mnupwd  44841  ismnushort  44875  iinssf  45714  founiiun  45755  founiiun0  45766  climuzlem  46315  stirlinglem13  46658  fourierdlem112  46790  2reuimp0  47706  2reuimp  47707  gbogbow  48376  sbgoldbo  48407  iineq0  49449  iuneqconst2  49452  iineqconst2  49453  sepcsepo  49556  seppsepf  49558