Theorem reximi 3068

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  r19.35  3089  r19.35OLD  3090  r19.29rOLD  3098  r19.40  3100  2r19.29  3120  2reu2rex  3370  reu3  3701  2reu5  3732  reuan  3862  dfiun2g  4997  ssiun  5013  iinss  5023  elsnxp  6267  elunirn  7228  el2xpss  8019  iiner  8765  erovlem  8789  xpf1o  9109  enp1i  9231  unbnn2  9251  scott0  9846  dfac2b  10091  cflm  10210  alephsing  10236  numthcor  10454  zorng  10464  zornn0g  10465  ttukeyg  10477  uniimadom  10504  axgroth3  10791  qextlt  13170  qextle  13171  mptnn0fsuppd  13970  hashgt23el  14396  hash2sspr  14461  cshword  14763  rexanre  15320  climi2  15484  climi0  15485  rlimres  15531  lo1res  15532  caurcvgr  15647  caurcvg2  15651  caucvgb  15653  prodmolem2  15908  prodmo  15909  vdwnnlem1  16973  cshwsiun  17077  isnmnd  18672  efgrelexlemb  19687  nn0gsumfz0  19922  ablsimpgfind  20049  rhmdvdsr  20424  pmatcollpw2lem  22671  eltg2b  22853  neiptopuni  23024  neiptopnei  23026  ordtbas2  23085  lmcvg  23156  cnprest  23183  lmcnp  23198  nrmsep2  23250  bwth  23304  1stcfb  23339  islly2  23378  llycmpkgen  23446  txbas  23461  tx1stc  23544  cnextcn  23961  tmdcn2  23983  utoptop  24129  ucnima  24175  cfiluweak  24189  metrest  24419  metust  24453  cfilucfil  24454  metustbl  24461  xrhmeo  24851  cmetcaulem  25195  iundisj  25456  limcresi  25793  elply2  26108  aalioulem2  26248  ulmf  26298  lgamucov2  26956  2sqlem7  27342  2sqreultblem  27366  2sqreunnltblem  27369  pntrsumbnd  27484  nosupno  27622  nosupfv  27625  noinfno  27637  noinffv  27640  istrkg2ld  28394  tgisline  28561  umgr2edgneu  29148  umgr3v3e3cycl  30120  eucrctshift  30179  1to3vfriendship  30217  2pthfrgrrn  30218  grpoidval  30449  grporcan  30454  grpoinveu  30455  iunrnmptss  32501  iundisjf  32525  xlt2addrd  32689  xrofsup  32697  iundisjfi  32726  isdrng4  33252  tpr2rico  33909  esumc  34048  esumfsup  34067  esumpcvgval  34075  hasheuni  34082  esumiun  34091  voliune  34226  volfiniune  34227  dya2icoseg2  34276  dya2iocnei  34280  dya2iocuni  34281  omssubaddlem  34297  omssubadd  34298  afsval  34669  bnj31  34716  bnj1239  34802  bnj900  34926  bnj906  34927  bnj1398  35031  bnj1498  35058  nummin  35088  onvf1odlem1  35097  satfvsuclem1  35353  satfv1  35357  satfvsucsuc  35359  colinearex  36055  segcon2  36100  opnrebl2  36316  nlpfvineqsn  37404  fvineqsneq  37407  pibt2  37412  sdclem2  37743  heibor1lem  37810  grpomndo  37876  disjdmqsss  38801  disjdmqscossss  38802  dmqsblocks  38852  prtlem9  38864  prter1  38879  prter2  38881  hl2at  39406  cvrval4N  39415  athgt  39457  1dimN  39472  lhpexnle  40007  lhpexle1  40009  cdlemftr2  40567  cdlemftr1  40568  cdlemftr0  40569  cdlemg5  40606  cdlemg33c0  40703  mapdrvallem2  41646  sn-negex  42413  sn-negex2  42414  eldiophb  42752  rmxyelqirr  42905  rmxyelqirrOLD  42906  hbtlem1  43119  hbtlem7  43121  ss2iundf  43655  mnupwd  44263  ismnushort  44297  iinssf  45139  founiiun  45180  founiiun0  45191  climuzlem  45748  stirlinglem13  46091  fourierdlem112  46223  2reuimp0  47119  2reuimp  47120  gbogbow  47761  sbgoldbo  47792  iineq0  48812  iuneqconst2  48815  iineqconst2  48816  sepcsepo  48919  seppsepf  48921