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 2114  ∃wrex 3061

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 3062

This theorem is referenced by:  r19.35  3095  r19.40  3103  2r19.29  3123  2reu2rex  3363  reu3  3686  2reu5  3717  reuan  3847  dfiun2g  4986  ssiun  5003  iinss  5013  elsnxp  6250  elunirn  7199  el2xpss  7983  iiner  8730  erovlem  8754  xpf1o  9071  enp1i  9183  unbnn2  9201  scott0  9802  dfac2b  10045  cflm  10164  alephsing  10190  numthcor  10408  zorng  10418  zornn0g  10419  ttukeyg  10431  uniimadom  10458  axgroth3  10746  qextlt  13122  qextle  13123  mptnn0fsuppd  13925  hashgt23el  14351  hash2sspr  14416  cshword  14718  rexanre  15274  climi2  15438  climi0  15439  rlimres  15485  lo1res  15486  caurcvgr  15601  caurcvg2  15605  caucvgb  15607  prodmolem2  15862  prodmo  15863  vdwnnlem1  16927  cshwsiun  17031  isnmnd  18667  efgrelexlemb  19683  nn0gsumfz0  19918  ablsimpgfind  20045  rhmdvdsr  20445  pmatcollpw2lem  22725  eltg2b  22907  neiptopuni  23078  neiptopnei  23080  ordtbas2  23139  lmcvg  23210  cnprest  23237  lmcnp  23252  nrmsep2  23304  bwth  23358  1stcfb  23393  islly2  23432  llycmpkgen  23500  txbas  23515  tx1stc  23598  cnextcn  24015  tmdcn2  24037  utoptop  24182  ucnima  24228  cfiluweak  24242  metrest  24472  metust  24506  cfilucfil  24507  metustbl  24514  xrhmeo  24904  cmetcaulem  25248  iundisj  25509  limcresi  25846  elply2  26161  aalioulem2  26301  ulmf  26351  lgamucov2  27009  2sqlem7  27395  2sqreultblem  27419  2sqreunnltblem  27422  pntrsumbnd  27537  nosupno  27675  nosupfv  27678  noinfno  27690  noinffv  27693  istrkg2ld  28515  tgisline  28682  umgr2edgneu  29270  umgr3v3e3cycl  30242  eucrctshift  30301  1to3vfriendship  30339  2pthfrgrrn  30340  grpoidval  30571  grporcan  30576  grpoinveu  30577  iunrnmptss  32622  iundisjf  32646  xlt2addrd  32820  xrofsup  32828  iundisjfi  32857  isdrng4  33358  tpr2rico  34050  esumc  34189  esumfsup  34208  esumpcvgval  34216  hasheuni  34223  esumiun  34232  voliune  34367  volfiniune  34368  dya2icoseg2  34416  dya2iocnei  34420  dya2iocuni  34421  omssubaddlem  34437  omssubadd  34438  afsval  34809  bnj31  34856  bnj1239  34942  bnj900  35066  bnj906  35067  bnj1398  35171  bnj1498  35198  nummin  35230  r1omhf  35243  noinfepregs  35270  onvf1odlem1  35278  satfvsuclem1  35534  satfv1  35538  satfvsucsuc  35540  colinearex  36235  segcon2  36280  opnrebl2  36496  nlpfvineqsn  37585  fvineqsneq  37588  pibt2  37593  sdclem2  37914  heibor1lem  37981  grpomndo  38047  disjdmqsss  39077  disjdmqscossss  39078  dmqsblocks  39139  prtlem9  39161  prter1  39176  prter2  39178  hl2at  39702  cvrval4N  39711  athgt  39753  1dimN  39768  lhpexnle  40303  lhpexle1  40305  cdlemftr2  40863  cdlemftr1  40864  cdlemftr0  40865  cdlemg5  40902  cdlemg33c0  40999  mapdrvallem2  41942  sn-negex  42709  sn-negex2  42710  eldiophb  43035  rmxyelqirr  43188  hbtlem1  43401  hbtlem7  43403  ss2iundf  43936  mnupwd  44544  ismnushort  44578  iinssf  45418  founiiun  45459  founiiun0  45470  climuzlem  46023  stirlinglem13  46366  fourierdlem112  46498  2reuimp0  47396  2reuimp  47397  gbogbow  48038  sbgoldbo  48069  iineq0  49101  iuneqconst2  49104  iineqconst2  49105  sepcsepo  49208  seppsepf  49210