Theorem reximi 3075

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

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

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 3062

This theorem is referenced by:  r19.35  3096  r19.35OLD  3097  r19.29rOLD  3105  r19.40  3107  2r19.29  3127  2reu2rex  3378  reu3  3715  2reu5  3746  reuan  3876  dfiun2g  5011  ssiun  5027  iinss  5037  elsnxp  6285  elunirn  7248  el2xpss  8041  iiner  8808  erovlem  8832  xpf1o  9158  enp1i  9290  unbnn2  9310  scott0  9905  dfac2b  10150  cflm  10269  alephsing  10295  numthcor  10513  zorng  10523  zornn0g  10524  ttukeyg  10536  uniimadom  10563  axgroth3  10850  qextlt  13224  qextle  13225  mptnn0fsuppd  14021  hashgt23el  14447  hash2sspr  14512  cshword  14814  rexanre  15370  climi2  15532  climi0  15533  rlimres  15579  lo1res  15580  caurcvgr  15695  caurcvg2  15699  caucvgb  15701  prodmolem2  15956  prodmo  15957  vdwnnlem1  17020  cshwsiun  17124  isnmnd  18721  efgrelexlemb  19736  nn0gsumfz0  19971  ablsimpgfind  20098  rhmdvdsr  20473  pmatcollpw2lem  22720  eltg2b  22902  neiptopuni  23073  neiptopnei  23075  ordtbas2  23134  lmcvg  23205  cnprest  23232  lmcnp  23247  nrmsep2  23299  bwth  23353  1stcfb  23388  islly2  23427  llycmpkgen  23495  txbas  23510  tx1stc  23593  cnextcn  24010  tmdcn2  24032  utoptop  24178  ucnima  24224  cfiluweak  24238  metrest  24468  metust  24502  cfilucfil  24503  metustbl  24510  xrhmeo  24900  cmetcaulem  25245  iundisj  25506  limcresi  25843  elply2  26158  aalioulem2  26298  ulmf  26348  lgamucov2  27006  2sqlem7  27392  2sqreultblem  27416  2sqreunnltblem  27419  pntrsumbnd  27534  nosupno  27672  nosupfv  27675  noinfno  27687  noinffv  27690  istrkg2ld  28444  tgisline  28611  umgr2edgneu  29198  umgr3v3e3cycl  30170  eucrctshift  30229  1to3vfriendship  30267  2pthfrgrrn  30268  grpoidval  30499  grporcan  30504  grpoinveu  30505  iunrnmptss  32551  iundisjf  32575  xlt2addrd  32741  xrofsup  32749  iundisjfi  32778  isdrng4  33294  tpr2rico  33948  esumc  34087  esumfsup  34106  esumpcvgval  34114  hasheuni  34121  esumiun  34130  voliune  34265  volfiniune  34266  dya2icoseg2  34315  dya2iocnei  34319  dya2iocuni  34320  omssubaddlem  34336  omssubadd  34337  afsval  34708  bnj31  34755  bnj1239  34841  bnj900  34965  bnj906  34966  bnj1398  35070  bnj1498  35097  nummin  35127  satfvsuclem1  35386  satfv1  35390  satfvsucsuc  35392  colinearex  36083  segcon2  36128  opnrebl2  36344  nlpfvineqsn  37432  fvineqsneq  37435  pibt2  37440  sdclem2  37771  heibor1lem  37838  grpomndo  37904  disjdmqsss  38825  disjdmqscossss  38826  prtlem9  38887  prter1  38902  prter2  38904  hl2at  39429  cvrval4N  39438  athgt  39480  1dimN  39495  lhpexnle  40030  lhpexle1  40032  cdlemftr2  40590  cdlemftr1  40591  cdlemftr0  40592  cdlemg5  40629  cdlemg33c0  40726  mapdrvallem2  41669  sn-negex  42435  sn-negex2  42436  eldiophb  42755  rmxyelqirr  42908  rmxyelqirrOLD  42909  hbtlem1  43122  hbtlem7  43124  ss2iundf  43658  mnupwd  44266  ismnushort  44300  iinssf  45142  founiiun  45183  founiiun0  45194  climuzlem  45752  stirlinglem13  46095  fourierdlem112  46227  2reuimp0  47123  2reuimp  47124  gbogbow  47750  sbgoldbo  47781  iineq0  48778  iuneqconst2  48781  iineqconst2  48782  sepcsepo  48881  seppsepf  48883