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  6256  elunirn  7206  el2xpss  7990  iiner  8736  erovlem  8760  xpf1o  9077  enp1i  9189  unbnn2  9207  scott0  9810  dfac2b  10053  cflm  10172  alephsing  10198  numthcor  10416  zorng  10426  zornn0g  10427  ttukeyg  10439  uniimadom  10466  axgroth3  10754  qextlt  13155  qextle  13156  mptnn0fsuppd  13960  hashgt23el  14386  hash2sspr  14451  cshword  14753  rexanre  15309  climi2  15473  climi0  15474  rlimres  15520  lo1res  15521  caurcvgr  15636  caurcvg2  15640  caucvgb  15642  prodmolem2  15900  prodmo  15901  vdwnnlem1  16966  cshwsiun  17070  isnmnd  18706  efgrelexlemb  19725  nn0gsumfz0  19960  ablsimpgfind  20087  rhmdvdsr  20485  pmatcollpw2lem  22742  eltg2b  22924  neiptopuni  23095  neiptopnei  23097  ordtbas2  23156  lmcvg  23227  cnprest  23254  lmcnp  23269  nrmsep2  23321  bwth  23375  1stcfb  23410  islly2  23449  llycmpkgen  23517  txbas  23532  tx1stc  23615  cnextcn  24032  tmdcn2  24054  utoptop  24199  ucnima  24245  cfiluweak  24259  metrest  24489  metust  24523  cfilucfil  24524  metustbl  24531  xrhmeo  24913  cmetcaulem  25255  iundisj  25515  limcresi  25852  elply2  26161  aalioulem2  26299  ulmf  26347  lgamucov2  27002  2sqlem7  27387  2sqreultblem  27411  2sqreunnltblem  27414  pntrsumbnd  27529  nosupno  27667  nosupfv  27670  noinfno  27682  noinffv  27685  istrkg2ld  28528  tgisline  28695  umgr2edgneu  29283  umgr3v3e3cycl  30254  eucrctshift  30313  1to3vfriendship  30351  2pthfrgrrn  30352  grpoidval  30584  grporcan  30589  grpoinveu  30590  iunrnmptss  32635  iundisjf  32659  xlt2addrd  32832  xrofsup  32840  iundisjfi  32869  isdrng4  33356  tpr2rico  34056  esumc  34195  esumfsup  34214  esumpcvgval  34222  hasheuni  34229  esumiun  34238  voliune  34373  volfiniune  34374  dya2icoseg2  34422  dya2iocnei  34426  dya2iocuni  34427  omssubaddlem  34443  omssubadd  34444  afsval  34815  bnj31  34862  bnj1239  34947  bnj900  35071  bnj906  35072  bnj1398  35176  bnj1498  35203  nummin  35236  r1omhf  35249  noinfepregs  35277  onvf1odlem1  35285  satfvsuclem1  35541  satfv1  35545  satfvsucsuc  35547  colinearex  36242  segcon2  36287  opnrebl2  36503  regsfromunir1  36722  nlpfvineqsn  37725  fvineqsneq  37728  pibt2  37733  sdclem2  38063  heibor1lem  38130  grpomndo  38196  disjdmqsss  39226  disjdmqscossss  39227  dmqsblocks  39288  prtlem9  39310  prter1  39325  prter2  39327  hl2at  39851  cvrval4N  39860  athgt  39902  1dimN  39917  lhpexnle  40452  lhpexle1  40454  cdlemftr2  41012  cdlemftr1  41013  cdlemftr0  41014  cdlemg5  41051  cdlemg33c0  41148  mapdrvallem2  42091  sn-negex  42850  sn-negex2  42851  eldiophb  43189  rmxyelqirr  43338  hbtlem1  43551  hbtlem7  43553  ss2iundf  44086  mnupwd  44694  ismnushort  44728  iinssf  45568  founiiun  45609  founiiun0  45620  climuzlem  46171  stirlinglem13  46514  fourierdlem112  46646  2reuimp0  47556  2reuimp  47557  gbogbow  48226  sbgoldbo  48257  iineq0  49289  iuneqconst2  49292  iineqconst2  49293  sepcsepo  49396  seppsepf  49398