Theorem reximi 3040

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
reximi	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	reximia 3038	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2030  ∃wrex 2942

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947

This theorem is referenced by:  2r19.29  3108  r19.29d2r  3109  r19.40  3117  reu3  3429  2reu5  3449  ssiun  4594  iinss  4603  elsnxp  5715  elsnxpOLD  5716  elunirn  6549  iiner  7862  erovlem  7886  xpf1o  8163  unbnn2  8258  scott0  8787  dfac2  8991  cflm  9110  alephsing  9136  numthcor  9354  zorng  9364  zornn0g  9365  ttukeyg  9377  uniimadom  9404  axgroth3  9691  qextlt  12072  qextle  12073  mptnn0fsuppd  12838  hash2sspr  13308  cshword  13583  rexanre  14130  climi2  14286  climi0  14287  rlimres  14333  lo1res  14334  caurcvgr  14448  caurcvg2  14452  caucvgb  14454  prodmolem2  14709  prodmo  14710  vdwnnlem1  15746  cshwsiun  15853  isnmnd  17345  efgrelexlemb  18209  nn0gsumfz0  18427  pmatcollpw2lem  20630  eltg2b  20811  neiptopuni  20982  neiptopnei  20984  ordtbas2  21043  lmcvg  21114  cnprest  21141  lmcnp  21156  nrmsep2  21208  bwth  21261  1stcfb  21296  islly2  21335  llycmpkgen  21403  txbas  21418  tx1stc  21501  cnextcn  21918  tmdcn2  21940  utoptop  22085  ucnima  22132  cfiluweak  22146  metrest  22376  metust  22410  cfilucfil  22411  metustbl  22418  xrhmeo  22792  cmetcaulem  23132  iundisj  23362  limcresi  23694  elply2  23997  aalioulem2  24133  ulmf  24181  lgamucov2  24810  2sqlem7  25194  pntrsumbnd  25300  istrkg2ld  25404  tgisline  25567  umgr2edgneu  26151  umgr3v3e3cycl  27162  eucrctshift  27221  1to3vfriendship  27261  2pthfrgrrn  27262  grpoidval  27495  grporcan  27500  grpoinveu  27501  iundisjf  29528  xlt2addrd  29651  xrofsup  29661  iundisjfi  29683  rhmdvdsr  29946  tpr2rico  30086  esumc  30241  esumfsup  30260  esumpcvgval  30268  hasheuni  30275  esumiun  30284  voliune  30420  volfiniune  30421  dya2icoseg2  30468  dya2iocnei  30472  dya2iocuni  30473  omssubaddlem  30489  omssubadd  30490  afsval  30877  bnj31  30913  bnj1239  31002  bnj900  31125  bnj906  31126  bnj1398  31228  bnj1498  31255  nosupno  31974  nosupfv  31977  colinearex  32292  segcon2  32337  opnrebl2  32441  sdclem2  33668  heibor1lem  33738  grpomndo  33804  prtlem9  34468  prtlem11  34470  prter1  34483  prter2  34485  hl2at  35009  cvrval4N  35018  athgt  35060  1dimN  35075  lhpexnle  35610  lhpexle1  35612  cdlemftr2  36171  cdlemftr1  36172  cdlemftr0  36173  cdlemg5  36210  cdlemg33c0  36307  mapdrvallem2  37251  eldiophb  37637  rmxyelqirr  37792  hbtlem1  38010  hbtlem7  38012  ss2iundf  38268  iinssf  39641  founiiun  39674  founiiun0  39691  climuzlem  40293  stirlinglem13  40621  fourierdlem112  40753  reuan  41501  2reu2rex  41504  cshword2  41762  gbogbow  41969  sbgoldbo  42000