Theorem reximi 3067

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

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

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 3054

This theorem is referenced by:  r19.35  3087  r19.40  3095  2r19.29  3115  2reu2rex  3359  reu3  3689  2reu5  3720  reuan  3850  dfiun2g  4983  ssiun  4998  iinss  5008  elsnxp  6243  elunirn  7191  el2xpss  7979  iiner  8723  erovlem  8747  xpf1o  9063  enp1i  9182  unbnn2  9202  scott0  9801  dfac2b  10044  cflm  10163  alephsing  10189  numthcor  10407  zorng  10417  zornn0g  10418  ttukeyg  10430  uniimadom  10457  axgroth3  10744  qextlt  13123  qextle  13124  mptnn0fsuppd  13923  hashgt23el  14349  hash2sspr  14414  cshword  14715  rexanre  15272  climi2  15436  climi0  15437  rlimres  15483  lo1res  15484  caurcvgr  15599  caurcvg2  15603  caucvgb  15605  prodmolem2  15860  prodmo  15861  vdwnnlem1  16925  cshwsiun  17029  isnmnd  18630  efgrelexlemb  19647  nn0gsumfz0  19882  ablsimpgfind  20009  rhmdvdsr  20411  pmatcollpw2lem  22680  eltg2b  22862  neiptopuni  23033  neiptopnei  23035  ordtbas2  23094  lmcvg  23165  cnprest  23192  lmcnp  23207  nrmsep2  23259  bwth  23313  1stcfb  23348  islly2  23387  llycmpkgen  23455  txbas  23470  tx1stc  23553  cnextcn  23970  tmdcn2  23992  utoptop  24138  ucnima  24184  cfiluweak  24198  metrest  24428  metust  24462  cfilucfil  24463  metustbl  24470  xrhmeo  24860  cmetcaulem  25204  iundisj  25465  limcresi  25802  elply2  26117  aalioulem2  26257  ulmf  26307  lgamucov2  26965  2sqlem7  27351  2sqreultblem  27375  2sqreunnltblem  27378  pntrsumbnd  27493  nosupno  27631  nosupfv  27634  noinfno  27646  noinffv  27649  istrkg2ld  28423  tgisline  28590  umgr2edgneu  29177  umgr3v3e3cycl  30146  eucrctshift  30205  1to3vfriendship  30243  2pthfrgrrn  30244  grpoidval  30475  grporcan  30480  grpoinveu  30481  iunrnmptss  32527  iundisjf  32551  xlt2addrd  32715  xrofsup  32723  iundisjfi  32752  isdrng4  33244  tpr2rico  33878  esumc  34017  esumfsup  34036  esumpcvgval  34044  hasheuni  34051  esumiun  34060  voliune  34195  volfiniune  34196  dya2icoseg2  34245  dya2iocnei  34249  dya2iocuni  34250  omssubaddlem  34266  omssubadd  34267  afsval  34638  bnj31  34685  bnj1239  34771  bnj900  34895  bnj906  34896  bnj1398  35000  bnj1498  35027  nummin  35057  onvf1odlem1  35075  satfvsuclem1  35331  satfv1  35335  satfvsucsuc  35337  colinearex  36033  segcon2  36078  opnrebl2  36294  nlpfvineqsn  37382  fvineqsneq  37385  pibt2  37390  sdclem2  37721  heibor1lem  37788  grpomndo  37854  disjdmqsss  38779  disjdmqscossss  38780  dmqsblocks  38830  prtlem9  38842  prter1  38857  prter2  38859  hl2at  39384  cvrval4N  39393  athgt  39435  1dimN  39450  lhpexnle  39985  lhpexle1  39987  cdlemftr2  40545  cdlemftr1  40546  cdlemftr0  40547  cdlemg5  40584  cdlemg33c0  40681  mapdrvallem2  41624  sn-negex  42391  sn-negex2  42392  eldiophb  42730  rmxyelqirr  42883  hbtlem1  43096  hbtlem7  43098  ss2iundf  43632  mnupwd  44240  ismnushort  44274  iinssf  45116  founiiun  45157  founiiun0  45168  climuzlem  45725  stirlinglem13  46068  fourierdlem112  46200  2reuimp0  47099  2reuimp  47100  gbogbow  47741  sbgoldbo  47772  iineq0  48792  iuneqconst2  48795  iineqconst2  48796  sepcsepo  48899  seppsepf  48901