Theorem reximi 3100

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.35  3120  r19.40  3128  2r19.29  3148  2reu2rex  3377  reu3  3684  2reu5  3715  reuan  3843  dfiun2g  4987  ssiun  5004  iinss  5014  elsnxp  6294  elunirn  7255  el2xpss  8048  iiner  8811  erovlem  8835  xpf1o  9159  enp1i  9271  unbnn2  9290  scott0b  9938  scott0OLD  9939  dfac2b  10210  cflm  10328  alephsing  10355  numthcor  10573  zorng  10583  zornn0g  10584  ttukeyg  10596  uniimadom  10629  axgroth3  10917  qextlt  13334  qextle  13335  mptnn0fsuppd  14142  hashgt23el  14570  hash2sspr  14635  cshword  14943  rexanre  15515  climi2  15679  climi0  15680  rlimres  15726  lo1res  15727  caurcvgr  15842  caurcvg2  15846  caucvgb  15848  prodmolem2  16103  prodmo  16104  vdwnnlem1  17174  cshwsiun  17278  isnmnd  18928  efgrelexlemb  19965  nn0gsumfz0  20200  ablsimpgfind  20327  rhmdvdsr  20759  isdrng4  20993  pmatcollpw2lem  23096  eltg2b  23278  neiptopuni  23449  neiptopnei  23451  ordtbas2  23510  lmcvg  23581  cnprest  23608  lmcnp  23623  nrmsep2  23675  bwth  23729  1stcfb  23764  islly2  23804  llycmpkgen  23872  txbas  23887  tx1stc  23970  cnextcn  24387  tmdcn2  24409  utoptop  24554  ucnima  24600  cfiluweak  24614  metrest  24844  metust  24878  cfilucfil  24879  metustbl  24886  xrhmeo  25268  cmetcaulem  25610  iundisj  25870  limcresi  26206  elply2  26515  aalioulem2  26661  ulmf  26710  lgamucov2  27367  2sqlem7  27752  2sqreultblem  27776  2sqreunnltblem  27779  pntrsumbnd  27894  nosupno  28061  nosupfv  28064  noinfno  28076  noinffv  28079  istrkg2ld  28923  tgisline  29096  cgrabasimass  29379  umgr2edgneu  29796  umgr3v3e3cycl  30786  eucrctshift  30845  1to3vfriendship  30883  2pthfrgrrn  30884  grpoidval  31116  grporcan  31121  grpoinveu  31122  inagcgratrgncol  33058  iunrnmptss  33202  iundisjf  33226  xlt2addrd  33394  xrofsup  33402  iundisjfi  33431  dflringlem2  34070  tpr2rico  34587  esumc  34726  esumfsup  34745  esumpcvgval  34753  hasheuni  34760  esumiun  34769  voliune  34905  volfiniune  34906  dya2icoseg2  34953  dya2iocnei  34957  dya2iocuni  34958  omssubaddlem  34974  omssubadd  34975  afsval  35346  bnj31  35393  bnj1239  35478  bnj900  35602  bnj906  35603  bnj1398  35707  bnj1498  35734  nummin  35767  noinfepregs  35850  onvf1odlem1  35943  vonf1oonfo  35961  satfvsuclem1  36193  satfv1  36197  satfvsucsuc  36199  colinearex  36900  segcon2  36945  opnrebl2  37184  regsfromunir1  37403  nlpfvineqsn  38408  fvineqsneq  38411  pibt2  38416  negprop  38719  sdclem2  38752  heibor1lem  38819  grpomndo  38885  disjdmqsss  39913  disjdmqscossss  39914  dmqsblocks  39975  prtlem9  39997  prter1  40012  prter2  40014  hl2at  40538  cvrval4N  40547  athgt  40589  1dimN  40604  lhpexnle  41139  lhpexle1  41141  cdlemftr2  41699  cdlemftr1  41700  cdlemftr0  41701  cdlemg5  41738  cdlemg33c0  41835  mapdrvallem2  42778  sn-negex  43545  sn-negex2  43546  eldiophb  43844  rmxyelqirr  43993  hbtlem1  44201  hbtlem7  44203  ss2iundf  44735  mnupwd  45327  ismnushort  45361  dmstructnn  46002  dmstructfi  46003  iinssf  46229  founiiun  46270  founiiun0  46281  climuzlem  46829  stirlinglem13  47172  fourierdlem112  47304  2reuimp0  48260  2reuimp  48261  gbogbow  48930  sbgoldbo  48961  iineq0  50006  iuneqconst2  50009  iineqconst2  50010  sepcsepo  50111  seppsepf  50113