Theorem reximi 3076

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.35  3096  r19.40  3104  2r19.29  3124  2reu2rex  3355  reu3  3674  2reu5  3705  reuan  3835  dfiun2g  4973  ssiun  4990  iinss  5000  elsnxp  6247  elunirn  7197  el2xpss  7981  iiner  8727  erovlem  8751  xpf1o  9068  enp1i  9180  unbnn2  9198  scott0  9799  dfac2b  10042  cflm  10161  alephsing  10187  numthcor  10405  zorng  10415  zornn0g  10416  ttukeyg  10428  uniimadom  10455  axgroth3  10743  qextlt  13144  qextle  13145  mptnn0fsuppd  13949  hashgt23el  14375  hash2sspr  14440  cshword  14742  rexanre  15298  climi2  15462  climi0  15463  rlimres  15509  lo1res  15510  caurcvgr  15625  caurcvg2  15629  caucvgb  15631  prodmolem2  15889  prodmo  15890  vdwnnlem1  16955  cshwsiun  17059  isnmnd  18695  efgrelexlemb  19714  nn0gsumfz0  19949  ablsimpgfind  20076  rhmdvdsr  20474  pmatcollpw2lem  22751  eltg2b  22933  neiptopuni  23104  neiptopnei  23106  ordtbas2  23165  lmcvg  23236  cnprest  23263  lmcnp  23278  nrmsep2  23330  bwth  23384  1stcfb  23419  islly2  23458  llycmpkgen  23526  txbas  23541  tx1stc  23624  cnextcn  24041  tmdcn2  24063  utoptop  24208  ucnima  24254  cfiluweak  24268  metrest  24498  metust  24532  cfilucfil  24533  metustbl  24540  xrhmeo  24922  cmetcaulem  25264  iundisj  25524  limcresi  25861  elply2  26173  aalioulem2  26312  ulmf  26362  lgamucov2  27020  2sqlem7  27406  2sqreultblem  27430  2sqreunnltblem  27433  pntrsumbnd  27548  nosupno  27686  nosupfv  27689  noinfno  27701  noinffv  27704  istrkg2ld  28547  tgisline  28714  umgr2edgneu  29302  umgr3v3e3cycl  30274  eucrctshift  30333  1to3vfriendship  30371  2pthfrgrrn  30372  grpoidval  30604  grporcan  30609  grpoinveu  30610  iunrnmptss  32655  iundisjf  32679  xlt2addrd  32852  xrofsup  32860  iundisjfi  32889  isdrng4  33376  tpr2rico  34077  esumc  34216  esumfsup  34235  esumpcvgval  34243  hasheuni  34250  esumiun  34259  voliune  34394  volfiniune  34395  dya2icoseg2  34443  dya2iocnei  34447  dya2iocuni  34448  omssubaddlem  34464  omssubadd  34465  afsval  34836  bnj31  34883  bnj1239  34968  bnj900  35092  bnj906  35093  bnj1398  35197  bnj1498  35224  nummin  35257  r1omhf  35270  noinfepregs  35298  onvf1odlem1  35306  satfvsuclem1  35562  satfv1  35566  satfvsucsuc  35568  colinearex  36263  segcon2  36308  opnrebl2  36524  regsfromunir1  36743  nlpfvineqsn  37736  fvineqsneq  37739  pibt2  37744  sdclem2  38074  heibor1lem  38141  grpomndo  38207  disjdmqsss  39237  disjdmqscossss  39238  dmqsblocks  39299  prtlem9  39321  prter1  39336  prter2  39338  hl2at  39862  cvrval4N  39871  athgt  39913  1dimN  39928  lhpexnle  40463  lhpexle1  40465  cdlemftr2  41023  cdlemftr1  41024  cdlemftr0  41025  cdlemg5  41062  cdlemg33c0  41159  mapdrvallem2  42102  sn-negex  42861  sn-negex2  42862  eldiophb  43200  rmxyelqirr  43353  hbtlem1  43566  hbtlem7  43568  ss2iundf  44101  mnupwd  44709  ismnushort  44743  iinssf  45583  founiiun  45624  founiiun0  45635  climuzlem  46186  stirlinglem13  46529  fourierdlem112  46661  2reuimp0  47559  2reuimp  47560  gbogbow  48229  sbgoldbo  48260  iineq0  49292  iuneqconst2  49295  iineqconst2  49296  sepcsepo  49399  seppsepf  49401