Theorem reximi 3174

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  r19.29r  3184  2r19.29  3260  r19.29d2rOLD  3262  r19.29vvaOLD  3264  r19.35  3268  r19.40  3272  2reu2rex  3353  reu3  3657  2reu5  3688  reuan  3825  ssiun  4972  iinss  4982  elsnxp  6183  elunirn  7106  iiner  8536  erovlem  8560  xpf1o  8875  unbnn2  9001  scott0  9575  dfac2b  9817  cflm  9937  alephsing  9963  numthcor  10181  zorng  10191  zornn0g  10192  ttukeyg  10204  uniimadom  10231  axgroth3  10518  qextlt  12866  qextle  12867  mptnn0fsuppd  13646  hashgt23el  14067  hash2sspr  14130  cshword  14432  rexanre  14986  climi2  15148  climi0  15149  rlimres  15195  lo1res  15196  caurcvgr  15313  caurcvg2  15317  caucvgb  15319  prodmolem2  15573  prodmo  15574  vdwnnlem1  16624  cshwsiun  16729  isnmnd  18304  efgrelexlemb  19271  nn0gsumfz0  19501  ablsimpgfind  19628  pmatcollpw2lem  21834  eltg2b  22017  neiptopuni  22189  neiptopnei  22191  ordtbas2  22250  lmcvg  22321  cnprest  22348  lmcnp  22363  nrmsep2  22415  bwth  22469  1stcfb  22504  islly2  22543  llycmpkgen  22611  txbas  22626  tx1stc  22709  cnextcn  23126  tmdcn2  23148  utoptop  23294  ucnima  23341  cfiluweak  23355  metrest  23586  metust  23620  cfilucfil  23621  metustbl  23628  xrhmeo  24015  cmetcaulem  24357  iundisj  24617  limcresi  24954  elply2  25262  aalioulem2  25398  ulmf  25446  lgamucov2  26093  2sqlem7  26477  2sqreultblem  26501  2sqreunnltblem  26504  pntrsumbnd  26619  istrkg2ld  26725  tgisline  26892  umgr2edgneu  27484  umgr3v3e3cycl  28449  eucrctshift  28508  1to3vfriendship  28546  2pthfrgrrn  28547  grpoidval  28776  grporcan  28781  grpoinveu  28782  iunrnmptss  30806  iundisjf  30829  xlt2addrd  30983  xrofsup  30992  iundisjfi  31019  rhmdvdsr  31419  tpr2rico  31764  esumc  31919  esumfsup  31938  esumpcvgval  31946  hasheuni  31953  esumiun  31962  voliune  32097  volfiniune  32098  dya2icoseg2  32145  dya2iocnei  32149  dya2iocuni  32150  omssubaddlem  32166  omssubadd  32167  afsval  32551  bnj31  32598  bnj1239  32685  bnj900  32809  bnj906  32810  bnj1398  32914  bnj1498  32941  nummin  32963  satfvsuclem1  33221  satfv1  33225  satfvsucsuc  33227  elxpxpss  33587  nosupno  33833  nosupfv  33836  noinfno  33848  noinffv  33851  colinearex  34289  segcon2  34334  opnrebl2  34437  nlpfvineqsn  35507  fvineqsneq  35510  pibt2  35515  sdclem2  35827  heibor1lem  35894  grpomndo  35960  prtlem9  36805  prter1  36820  prter2  36822  hl2at  37346  cvrval4N  37355  athgt  37397  1dimN  37412  lhpexnle  37947  lhpexle1  37949  cdlemftr2  38507  cdlemftr1  38508  cdlemftr0  38509  cdlemg5  38546  cdlemg33c0  38643  mapdrvallem2  39586  sn-negex  40320  sn-negex2  40321  eldiophb  40495  rmxyelqirr  40648  hbtlem1  40864  hbtlem7  40866  ss2iundf  41156  mnupwd  41774  ismnushort  41808  iinssf  42576  founiiun  42604  founiiun0  42617  climuzlem  43174  stirlinglem13  43517  fourierdlem112  43649  2reuimp0  44493  2reuimp  44494  gbogbow  45096  sbgoldbo  45127  sepcsepo  46108  seppsepf  46110