Theorem reximi 3102

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∃wrex 3088

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

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-rex 3089

This theorem is used by:  r19.35  3122  r19.40  3130  2r19.29  3150  2reu2rex  3380  reu3  3689  2reu5  3720  reuan  3849  dfiun2g  4993  ssiun  5010  iinss  5020  elsnxp  6292  elunirn  7249  el2xpss  8032  iiner  8785  erovlem  8809  xpf1o  9125  enp1i  9237  unbnn2  9255  scott0b  9864  scott0OLD  9865  dfac2b  10121  cflm  10239  alephsing  10266  numthcor  10484  zorng  10494  zornn0g  10495  ttukeyg  10507  uniimadom  10534  axgroth3  10822  qextlt  13235  qextle  13236  mptnn0fsuppd  14041  hashgt23el  14468  hash2sspr  14533  cshword  14835  rexanre  15405  climi2  15569  climi0  15570  rlimres  15616  lo1res  15617  caurcvgr  15732  caurcvg2  15736  caucvgb  15738  prodmolem2  15996  prodmo  15997  vdwnnlem1  17061  cshwsiun  17165  isnmnd  18802  efgrelexlemb  19826  nn0gsumfz0  20061  ablsimpgfind  20188  rhmdvdsr  20616  isdrng4  20850  pmatcollpw2lem  22945  eltg2b  23127  neiptopuni  23298  neiptopnei  23300  ordtbas2  23359  lmcvg  23430  cnprest  23457  lmcnp  23472  nrmsep2  23524  bwth  23578  1stcfb  23613  islly2  23652  llycmpkgen  23720  txbas  23735  tx1stc  23818  cnextcn  24235  tmdcn2  24257  utoptop  24402  ucnima  24448  cfiluweak  24462  metrest  24692  metust  24726  cfilucfil  24727  metustbl  24734  xrhmeo  25116  cmetcaulem  25458  iundisj  25718  limcresi  26055  elply2  26364  aalioulem2  26507  ulmf  26556  lgamucov2  27214  2sqlem7  27599  2sqreultblem  27623  2sqreunnltblem  27626  pntrsumbnd  27741  nosupno  27878  nosupfv  27881  noinfno  27893  noinffv  27896  istrkg2ld  28740  tgisline  28911  umgr2edgneu  29575  umgr3v3e3cycl  30546  eucrctshift  30605  1to3vfriendship  30643  2pthfrgrrn  30644  grpoidval  30876  grporcan  30881  grpoinveu  30882  iunrnmptss  32921  iundisjf  32945  xlt2addrd  33115  xrofsup  33123  iundisjfi  33152  dflringlem2  33794  tpr2rico  34311  esumc  34450  esumfsup  34469  esumpcvgval  34477  hasheuni  34484  esumiun  34493  voliune  34628  volfiniune  34629  dya2icoseg2  34677  dya2iocnei  34681  dya2iocuni  34682  omssubaddlem  34698  omssubadd  34699  afsval  35070  bnj31  35117  bnj1239  35202  bnj900  35326  bnj906  35327  bnj1398  35431  bnj1498  35458  nummin  35493  r1omhf  35509  noinfepregs  35554  onvf1odlem1  35595  vonf1oonfo  35607  satfvsuclem1  35859  satfv1  35863  satfvsucsuc  35865  colinearex  36560  segcon2  36605  opnrebl2  36860  regsfromunir1  37079  nlpfvineqsn  38083  fvineqsneq  38086  pibt2  38091  sdclem2  38421  heibor1lem  38488  grpomndo  38554  disjdmqsss  39582  disjdmqscossss  39583  dmqsblocks  39644  prtlem9  39666  prter1  39681  prter2  39683  hl2at  40207  cvrval4N  40216  athgt  40258  1dimN  40273  lhpexnle  40808  lhpexle1  40810  cdlemftr2  41368  cdlemftr1  41369  cdlemftr0  41370  cdlemg5  41407  cdlemg33c0  41504  mapdrvallem2  42447  sn-negex  43207  sn-negex2  43208  eldiophb  43516  rmxyelqirr  43665  hbtlem1  43878  hbtlem7  43880  ss2iundf  44413  mnupwd  45005  ismnushort  45039  iinssf  45884  founiiun  45925  founiiun0  45936  climuzlem  46485  stirlinglem13  46828  fourierdlem112  46960  2reuimp0  47879  2reuimp  47880  gbogbow  48549  sbgoldbo  48580  iineq0  49626  iuneqconst2  49629  iineqconst2  49630  sepcsepo  49733  seppsepf  49735