Theorem reximi 3085

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

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

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 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.35  3109  r19.35OLD  3110  r19.29rOLD  3118  r19.40  3120  2r19.29  3140  r19.29d2rOLD  3142  r19.29vvaOLD  3215  2reu2rex  3391  reu3  3724  2reu5  3755  reuan  3891  dfiun2g  5034  ssiun  5050  iinss  5060  elsnxp  6291  elunirn  7250  el2xpss  8023  iiner  8783  erovlem  8807  xpf1o  9139  enp1i  9279  unbnn2  9300  scott0  9881  dfac2b  10125  cflm  10245  alephsing  10271  numthcor  10489  zorng  10499  zornn0g  10500  ttukeyg  10512  uniimadom  10539  axgroth3  10826  qextlt  13182  qextle  13183  mptnn0fsuppd  13963  hashgt23el  14384  hash2sspr  14449  cshword  14741  rexanre  15293  climi2  15455  climi0  15456  rlimres  15502  lo1res  15503  caurcvgr  15620  caurcvg2  15624  caucvgb  15626  prodmolem2  15879  prodmo  15880  vdwnnlem1  16928  cshwsiun  17033  isnmnd  18629  efgrelexlemb  19618  nn0gsumfz0  19853  ablsimpgfind  19980  rhmdvdsr  20287  pmatcollpw2lem  22279  eltg2b  22462  neiptopuni  22634  neiptopnei  22636  ordtbas2  22695  lmcvg  22766  cnprest  22793  lmcnp  22808  nrmsep2  22860  bwth  22914  1stcfb  22949  islly2  22988  llycmpkgen  23056  txbas  23071  tx1stc  23154  cnextcn  23571  tmdcn2  23593  utoptop  23739  ucnima  23786  cfiluweak  23800  metrest  24033  metust  24067  cfilucfil  24068  metustbl  24075  xrhmeo  24462  cmetcaulem  24805  iundisj  25065  limcresi  25402  elply2  25710  aalioulem2  25846  ulmf  25894  lgamucov2  26543  2sqlem7  26927  2sqreultblem  26951  2sqreunnltblem  26954  pntrsumbnd  27069  nosupno  27206  nosupfv  27209  noinfno  27221  noinffv  27224  istrkg2ld  27742  tgisline  27909  umgr2edgneu  28502  umgr3v3e3cycl  29468  eucrctshift  29527  1to3vfriendship  29565  2pthfrgrrn  29566  grpoidval  29797  grporcan  29802  grpoinveu  29803  iunrnmptss  31828  iundisjf  31851  xlt2addrd  32002  xrofsup  32011  iundisjfi  32038  isdrng4  32426  tpr2rico  32923  esumc  33080  esumfsup  33099  esumpcvgval  33107  hasheuni  33114  esumiun  33123  voliune  33258  volfiniune  33259  dya2icoseg2  33308  dya2iocnei  33312  dya2iocuni  33313  omssubaddlem  33329  omssubadd  33330  afsval  33714  bnj31  33761  bnj1239  33847  bnj900  33971  bnj906  33972  bnj1398  34076  bnj1498  34103  nummin  34125  satfvsuclem1  34381  satfv1  34385  satfvsucsuc  34387  colinearex  35063  segcon2  35108  opnrebl2  35254  nlpfvineqsn  36338  fvineqsneq  36341  pibt2  36346  sdclem2  36658  heibor1lem  36725  grpomndo  36791  disjdmqsss  37720  disjdmqscossss  37721  prtlem9  37782  prter1  37797  prter2  37799  hl2at  38324  cvrval4N  38333  athgt  38375  1dimN  38390  lhpexnle  38925  lhpexle1  38927  cdlemftr2  39485  cdlemftr1  39486  cdlemftr0  39487  cdlemg5  39524  cdlemg33c0  39621  mapdrvallem2  40564  sn-negex  41338  sn-negex2  41339  eldiophb  41543  rmxyelqirr  41696  rmxyelqirrOLD  41697  hbtlem1  41913  hbtlem7  41915  ss2iundf  42458  mnupwd  43074  ismnushort  43108  iinssf  43875  founiiun  43923  founiiun0  43936  climuzlem  44507  stirlinglem13  44850  fourierdlem112  44982  2reuimp0  45870  2reuimp  45871  gbogbow  46472  sbgoldbo  46503  sepcsepo  47607  seppsepf  47609