Theorem reximi 3101

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 3087

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-rex 3088

This theorem is referenced by:  r19.35  3121  r19.40  3129  2r19.29  3149  2reu2rex  3379  reu3  3689  2reu5  3720  reuan  3849  dfiun2g  4993  ssiun  5010  iinss  5020  elsnxp  6292  elunirn  7249  el2xpss  8033  iiner  8786  erovlem  8810  xpf1o  9126  enp1i  9238  unbnn2  9256  scott0  9859  dfac2b  10113  cflm  10232  alephsing  10259  numthcor  10477  zorng  10487  zornn0g  10488  ttukeyg  10500  uniimadom  10527  axgroth3  10815  qextlt  13228  qextle  13229  mptnn0fsuppd  14034  hashgt23el  14461  hash2sspr  14526  cshword  14828  rexanre  15398  climi2  15562  climi0  15563  rlimres  15609  lo1res  15610  caurcvgr  15725  caurcvg2  15729  caucvgb  15731  prodmolem2  15989  prodmo  15990  vdwnnlem1  17054  cshwsiun  17158  isnmnd  18795  efgrelexlemb  19819  nn0gsumfz0  20054  ablsimpgfind  20181  rhmdvdsr  20590  isdrng4  20824  pmatcollpw2lem  22913  eltg2b  23095  neiptopuni  23266  neiptopnei  23268  ordtbas2  23327  lmcvg  23398  cnprest  23425  lmcnp  23440  nrmsep2  23492  bwth  23546  1stcfb  23581  islly2  23620  llycmpkgen  23688  txbas  23703  tx1stc  23786  cnextcn  24203  tmdcn2  24225  utoptop  24370  ucnima  24416  cfiluweak  24430  metrest  24660  metust  24694  cfilucfil  24695  metustbl  24702  xrhmeo  25084  cmetcaulem  25426  iundisj  25686  limcresi  26023  elply2  26332  aalioulem2  26473  ulmf  26521  lgamucov2  27179  2sqlem7  27564  2sqreultblem  27588  2sqreunnltblem  27591  pntrsumbnd  27706  nosupno  27843  nosupfv  27846  noinfno  27858  noinffv  27861  istrkg2ld  28705  tgisline  28876  umgr2edgneu  29530  umgr3v3e3cycl  30501  eucrctshift  30560  1to3vfriendship  30598  2pthfrgrrn  30599  grpoidval  30831  grporcan  30836  grpoinveu  30837  iunrnmptss  32876  iundisjf  32900  xlt2addrd  33070  xrofsup  33078  iundisjfi  33107  dflringlem2  33751  tpr2rico  34268  esumc  34407  esumfsup  34426  esumpcvgval  34434  hasheuni  34441  esumiun  34450  voliune  34585  volfiniune  34586  dya2icoseg2  34634  dya2iocnei  34638  dya2iocuni  34639  omssubaddlem  34655  omssubadd  34656  afsval  35027  bnj31  35074  bnj1239  35159  bnj900  35283  bnj906  35284  bnj1398  35388  bnj1498  35415  nummin  35450  r1omhf  35466  noinfepregs  35512  onvf1odlem1  35553  vonf1oonfo  35565  satfvsuclem1  35817  satfv1  35821  satfvsucsuc  35823  colinearex  36518  segcon2  36563  opnrebl2  36798  regsfromunir1  37017  nlpfvineqsn  38021  fvineqsneq  38024  pibt2  38029  sdclem2  38359  heibor1lem  38426  grpomndo  38492  disjdmqsss  39522  disjdmqscossss  39523  dmqsblocks  39584  prtlem9  39606  prter1  39621  prter2  39623  hl2at  40147  cvrval4N  40156  athgt  40198  1dimN  40213  lhpexnle  40748  lhpexle1  40750  cdlemftr2  41308  cdlemftr1  41309  cdlemftr0  41310  cdlemg5  41347  cdlemg33c0  41444  mapdrvallem2  42387  sn-negex  43147  sn-negex2  43148  eldiophb  43458  rmxyelqirr  43607  hbtlem1  43820  hbtlem7  43822  ss2iundf  44355  mnupwd  44947  ismnushort  44981  iinssf  45826  founiiun  45867  founiiun0  45878  climuzlem  46427  stirlinglem13  46770  fourierdlem112  46902  2reuimp0  47818  2reuimp  47819  gbogbow  48488  sbgoldbo  48519  iineq0  49565  iuneqconst2  49568  iineqconst2  49569  sepcsepo  49672  seppsepf  49674