Theorem reximi 3090

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.35  3114  r19.35OLD  3115  r19.29rOLD  3123  r19.40  3125  2r19.29  3145  r19.29d2rOLD  3147  r19.29vvaOLD  3223  2reu2rex  3402  reu3  3749  2reu5  3780  reuan  3918  dfiun2g  5053  ssiun  5069  iinss  5079  elsnxp  6322  elunirn  7288  el2xpss  8078  iiner  8847  erovlem  8871  xpf1o  9205  enp1i  9341  unbnn2  9361  scott0  9955  dfac2b  10200  cflm  10319  alephsing  10345  numthcor  10563  zorng  10573  zornn0g  10574  ttukeyg  10586  uniimadom  10613  axgroth3  10900  qextlt  13265  qextle  13266  mptnn0fsuppd  14049  hashgt23el  14473  hash2sspr  14538  cshword  14839  rexanre  15395  climi2  15557  climi0  15558  rlimres  15604  lo1res  15605  caurcvgr  15722  caurcvg2  15726  caucvgb  15728  prodmolem2  15983  prodmo  15984  vdwnnlem1  17042  cshwsiun  17147  isnmnd  18776  efgrelexlemb  19792  nn0gsumfz0  20027  ablsimpgfind  20154  rhmdvdsr  20534  pmatcollpw2lem  22804  eltg2b  22987  neiptopuni  23159  neiptopnei  23161  ordtbas2  23220  lmcvg  23291  cnprest  23318  lmcnp  23333  nrmsep2  23385  bwth  23439  1stcfb  23474  islly2  23513  llycmpkgen  23581  txbas  23596  tx1stc  23679  cnextcn  24096  tmdcn2  24118  utoptop  24264  ucnima  24311  cfiluweak  24325  metrest  24558  metust  24592  cfilucfil  24593  metustbl  24600  xrhmeo  24996  cmetcaulem  25341  iundisj  25602  limcresi  25940  elply2  26255  aalioulem2  26393  ulmf  26443  lgamucov2  27100  2sqlem7  27486  2sqreultblem  27510  2sqreunnltblem  27513  pntrsumbnd  27628  nosupno  27766  nosupfv  27769  noinfno  27781  noinffv  27784  istrkg2ld  28486  tgisline  28653  umgr2edgneu  29249  umgr3v3e3cycl  30216  eucrctshift  30275  1to3vfriendship  30313  2pthfrgrrn  30314  grpoidval  30545  grporcan  30550  grpoinveu  30551  iunrnmptss  32588  iundisjf  32611  xlt2addrd  32765  xrofsup  32774  iundisjfi  32801  isdrng4  33264  tpr2rico  33858  esumc  34015  esumfsup  34034  esumpcvgval  34042  hasheuni  34049  esumiun  34058  voliune  34193  volfiniune  34194  dya2icoseg2  34243  dya2iocnei  34247  dya2iocuni  34248  omssubaddlem  34264  omssubadd  34265  afsval  34648  bnj31  34695  bnj1239  34781  bnj900  34905  bnj906  34906  bnj1398  35010  bnj1498  35037  nummin  35067  satfvsuclem1  35327  satfv1  35331  satfvsucsuc  35333  colinearex  36024  segcon2  36069  opnrebl2  36287  nlpfvineqsn  37375  fvineqsneq  37378  pibt2  37383  sdclem2  37702  heibor1lem  37769  grpomndo  37835  disjdmqsss  38758  disjdmqscossss  38759  prtlem9  38820  prter1  38835  prter2  38837  hl2at  39362  cvrval4N  39371  athgt  39413  1dimN  39428  lhpexnle  39963  lhpexle1  39965  cdlemftr2  40523  cdlemftr1  40524  cdlemftr0  40525  cdlemg5  40562  cdlemg33c0  40659  mapdrvallem2  41602  sn-negex  42393  sn-negex2  42394  eldiophb  42713  rmxyelqirr  42866  rmxyelqirrOLD  42867  hbtlem1  43080  hbtlem7  43082  ss2iundf  43621  mnupwd  44236  ismnushort  44270  iinssf  45040  founiiun  45086  founiiun0  45097  climuzlem  45664  stirlinglem13  46007  fourierdlem112  46139  2reuimp0  47029  2reuimp  47030  gbogbow  47630  sbgoldbo  47661  sepcsepo  48606  seppsepf  48608