Theorem reximi 3078

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  r19.35  3098  r19.40  3106  2r19.29  3126  2reu2rex  3357  reu3  3675  2reu5  3706  reuan  3835  dfiun2g  4966  ssiun  4983  iinss  4993  elsnxp  6249  elunirn  7202  el2xpss  7986  iiner  8733  erovlem  8757  xpf1o  9074  enp1i  9186  unbnn2  9204  scott0  9808  dfac2b  10051  cflm  10170  alephsing  10196  numthcor  10414  zorng  10424  zornn0g  10425  ttukeyg  10437  uniimadom  10464  axgroth3  10752  qextlt  13153  qextle  13154  mptnn0fsuppd  13958  hashgt23el  14384  hash2sspr  14449  cshword  14751  rexanre  15307  climi2  15471  climi0  15472  rlimres  15518  lo1res  15519  caurcvgr  15634  caurcvg2  15638  caucvgb  15640  prodmolem2  15898  prodmo  15899  vdwnnlem1  16964  cshwsiun  17068  isnmnd  18704  efgrelexlemb  19723  nn0gsumfz0  19958  ablsimpgfind  20085  rhmdvdsr  20487  pmatcollpw2lem  22767  eltg2b  22949  neiptopuni  23120  neiptopnei  23122  ordtbas2  23181  lmcvg  23252  cnprest  23279  lmcnp  23294  nrmsep2  23346  bwth  23400  1stcfb  23435  islly2  23474  llycmpkgen  23542  txbas  23557  tx1stc  23640  cnextcn  24057  tmdcn2  24079  utoptop  24224  ucnima  24270  cfiluweak  24284  metrest  24514  metust  24548  cfilucfil  24549  metustbl  24556  xrhmeo  24938  cmetcaulem  25280  iundisj  25540  limcresi  25877  elply2  26186  aalioulem2  26324  ulmf  26372  lgamucov2  27027  2sqlem7  27412  2sqreultblem  27436  2sqreunnltblem  27439  pntrsumbnd  27554  nosupno  27692  nosupfv  27695  noinfno  27707  noinffv  27710  istrkg2ld  28553  tgisline  28720  umgr2edgneu  29308  umgr3v3e3cycl  30279  eucrctshift  30338  1to3vfriendship  30376  2pthfrgrrn  30377  grpoidval  30609  grporcan  30614  grpoinveu  30615  iunrnmptss  32661  iundisjf  32685  xlt2addrd  32858  xrofsup  32866  iundisjfi  32895  isdrng4  33386  tpr2rico  34103  esumc  34242  esumfsup  34261  esumpcvgval  34269  hasheuni  34276  esumiun  34285  voliune  34420  volfiniune  34421  dya2icoseg2  34469  dya2iocnei  34473  dya2iocuni  34474  omssubaddlem  34490  omssubadd  34491  afsval  34862  bnj31  34909  bnj1239  34994  bnj900  35118  bnj906  35119  bnj1398  35223  bnj1498  35250  nummin  35283  r1omhf  35296  noinfepregs  35324  onvf1odlem1  35332  satfvsuclem1  35588  satfv1  35592  satfvsucsuc  35594  colinearex  36289  segcon2  36334  opnrebl2  36550  regsfromunir1  36769  nlpfvineqsn  37772  fvineqsneq  37775  pibt2  37780  sdclem2  38110  heibor1lem  38177  grpomndo  38243  disjdmqsss  39273  disjdmqscossss  39274  dmqsblocks  39335  prtlem9  39357  prter1  39372  prter2  39374  hl2at  39898  cvrval4N  39907  athgt  39949  1dimN  39964  lhpexnle  40499  lhpexle1  40501  cdlemftr2  41059  cdlemftr1  41060  cdlemftr0  41061  cdlemg5  41098  cdlemg33c0  41195  mapdrvallem2  42138  sn-negex  42896  sn-negex2  42897  eldiophb  43207  rmxyelqirr  43356  hbtlem1  43569  hbtlem7  43571  ss2iundf  44104  mnupwd  44712  ismnushort  44746  iinssf  45586  founiiun  45627  founiiun0  45638  climuzlem  46187  stirlinglem13  46530  fourierdlem112  46662  2reuimp0  47578  2reuimp  47579  gbogbow  48248  sbgoldbo  48279  iineq0  49311  iuneqconst2  49314  iineqconst2  49315  sepcsepo  49418  seppsepf  49420