Theorem reximi 3179

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3066

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  r19.29r  3186  2r19.29  3264  r19.29d2rOLD  3266  r19.29vvaOLD  3268  r19.35  3272  r19.40  3276  2reu2rex  3364  reu3  3663  2reu5  3694  reuan  3830  dfiun2g  4961  ssiun  4977  iinss  4987  elsnxp  6198  elunirn  7133  iiner  8587  erovlem  8611  xpf1o  8935  unbnn2  9080  scott0  9653  dfac2b  9895  cflm  10015  alephsing  10041  numthcor  10259  zorng  10269  zornn0g  10270  ttukeyg  10282  uniimadom  10309  axgroth3  10596  qextlt  12946  qextle  12947  mptnn0fsuppd  13727  hashgt23el  14148  hash2sspr  14211  cshword  14513  rexanre  15067  climi2  15229  climi0  15230  rlimres  15276  lo1res  15277  caurcvgr  15394  caurcvg2  15398  caucvgb  15400  prodmolem2  15654  prodmo  15655  vdwnnlem1  16705  cshwsiun  16810  isnmnd  18398  efgrelexlemb  19365  nn0gsumfz0  19595  ablsimpgfind  19722  pmatcollpw2lem  21935  eltg2b  22118  neiptopuni  22290  neiptopnei  22292  ordtbas2  22351  lmcvg  22422  cnprest  22449  lmcnp  22464  nrmsep2  22516  bwth  22570  1stcfb  22605  islly2  22644  llycmpkgen  22712  txbas  22727  tx1stc  22810  cnextcn  23227  tmdcn2  23249  utoptop  23395  ucnima  23442  cfiluweak  23456  metrest  23689  metust  23723  cfilucfil  23724  metustbl  23731  xrhmeo  24118  cmetcaulem  24461  iundisj  24721  limcresi  25058  elply2  25366  aalioulem2  25502  ulmf  25550  lgamucov2  26197  2sqlem7  26581  2sqreultblem  26605  2sqreunnltblem  26608  pntrsumbnd  26723  istrkg2ld  26830  tgisline  26997  umgr2edgneu  27590  umgr3v3e3cycl  28557  eucrctshift  28616  1to3vfriendship  28654  2pthfrgrrn  28655  grpoidval  28884  grporcan  28889  grpoinveu  28890  iunrnmptss  30914  iundisjf  30937  xlt2addrd  31090  xrofsup  31099  iundisjfi  31126  rhmdvdsr  31526  tpr2rico  31871  esumc  32028  esumfsup  32047  esumpcvgval  32055  hasheuni  32062  esumiun  32071  voliune  32206  volfiniune  32207  dya2icoseg2  32254  dya2iocnei  32258  dya2iocuni  32259  omssubaddlem  32275  omssubadd  32276  afsval  32660  bnj31  32707  bnj1239  32794  bnj900  32918  bnj906  32919  bnj1398  33023  bnj1498  33050  nummin  33072  satfvsuclem1  33330  satfv1  33334  satfvsucsuc  33336  elxpxpss  33693  nosupno  33915  nosupfv  33918  noinfno  33930  noinffv  33933  colinearex  34371  segcon2  34416  opnrebl2  34519  nlpfvineqsn  35589  fvineqsneq  35592  pibt2  35597  sdclem2  35909  heibor1lem  35976  grpomndo  36042  prtlem9  36885  prter1  36900  prter2  36902  hl2at  37426  cvrval4N  37435  athgt  37477  1dimN  37492  lhpexnle  38027  lhpexle1  38029  cdlemftr2  38587  cdlemftr1  38588  cdlemftr0  38589  cdlemg5  38626  cdlemg33c0  38723  mapdrvallem2  39666  sn-negex  40406  sn-negex2  40407  eldiophb  40586  rmxyelqirr  40739  hbtlem1  40955  hbtlem7  40957  ss2iundf  41274  mnupwd  41892  ismnushort  41926  iinssf  42694  founiiun  42722  founiiun0  42735  climuzlem  43291  stirlinglem13  43634  fourierdlem112  43766  2reuimp0  44617  2reuimp  44618  gbogbow  45219  sbgoldbo  45250  sepcsepo  46231  seppsepf  46233