Theorem reximi 3104

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  r19.35  3124  r19.40  3132  2r19.29  3152  2reu2rex  3381  reu3  3688  2reu5  3719  reuan  3848  dfiun2g  4991  ssiun  5008  iinss  5018  elsnxp  6312  elunirn  7278  el2xpss  8072  iiner  8838  erovlem  8862  xpf1o  9186  enp1i  9298  unbnn2  9317  scott0b  9964  scott0OLD  9965  dfac2b  10236  cflm  10354  alephsing  10381  numthcor  10599  zorng  10609  zornn0g  10610  ttukeyg  10622  uniimadom  10655  axgroth3  10943  qextlt  13360  qextle  13361  mptnn0fsuppd  14168  hashgt23el  14596  hash2sspr  14661  cshword  14970  rexanre  15543  climi2  15707  climi0  15708  rlimres  15754  lo1res  15755  caurcvgr  15870  caurcvg2  15874  caucvgb  15876  prodmolem2  16131  prodmo  16132  vdwnnlem1  17202  cshwsiun  17306  isnmnd  18956  sgrpidmnd  18957  efgrelexlemb  19994  nn0gsumfz0  20229  ablsimpgfind  20356  rhmdvdsr  20788  isdrng4  21022  pmatcollpw2lem  23125  eltg2b  23307  neiptopuni  23478  neiptopnei  23480  ordtbas2  23539  lmcvg  23610  cnprest  23637  lmcnp  23652  nrmsep2  23704  bwth  23758  1stcfb  23793  islly2  23833  llycmpkgen  23901  txbas  23916  tx1stc  23999  cnextcn  24416  tmdcn2  24438  utoptop  24583  ucnima  24629  cfiluweak  24643  metrest  24873  metust  24907  cfilucfil  24908  metustbl  24915  xrhmeo  25297  cmetcaulem  25639  iundisj  25899  limcresi  26235  elply2  26544  aalioulem2  26690  ulmf  26739  lgamucov2  27396  2sqlem7  27781  2sqreultblem  27805  2sqreunnltblem  27808  pntrsumbnd  27923  nosupno  28090  nosupfv  28093  noinfno  28105  noinffv  28108  istrkg2ld  28952  tgisline  29125  cgrabasimass  29408  umgr2edgneu  29825  umgr3v3e3cycl  30815  eucrctshift  30874  1to3vfriendship  30912  2pthfrgrrn  30913  grpoidval  31145  grporcan  31150  grpoinveu  31151  inagcgratrgncol  33087  iunrnmptss  33231  iundisjf  33255  xlt2addrd  33421  xrofsup  33429  iundisjfi  33458  dflringlem2  34097  tpr2rico  34614  esumc  34753  esumfsup  34772  esumpcvgval  34780  hasheuni  34787  esumiun  34796  voliune  34932  volfiniune  34933  dya2icoseg2  34980  dya2iocnei  34984  dya2iocuni  34985  omssubaddlem  35001  omssubadd  35002  afsval  35373  bnj31  35420  bnj1239  35505  bnj900  35629  bnj906  35630  bnj1398  35734  bnj1498  35761  rmo6  35780  nummin  35806  noinfepregs  35901  onvf1odlem1  36031  vonf1oonfo  36049  satfvsuclem1  36291  satfv1  36295  satfvsucsuc  36297  colinearex  37003  segcon2  37048  opnrebl2  37287  regsfromunir1  37506  nlpfvineqsn  38524  fvineqsneq  38527  pibt2  38532  negprop  38835  sdclem2  38868  heibor1lem  38935  grpomndo  39001  disjdmqsss  40029  disjdmqscossss  40030  dmqsblocks  40091  prtlem9  40113  prter1  40128  prter2  40130  hl2at  40654  cvrval4N  40663  athgt  40705  1dimN  40720  lhpexnle  41255  lhpexle1  41257  cdlemftr2  41815  cdlemftr1  41816  cdlemftr0  41817  cdlemg5  41854  cdlemg33c0  41951  mapdrvallem2  42894  sn-negex  43662  sn-negex2  43663  eldiophb  43961  rmxyelqirr  44110  hbtlem1  44317  hbtlem7  44319  ss2iundf  44851  mnupwd  45443  ismnushort  45477  dmstructnn  46119  dmstructfi  46120  iinssf  46358  founiiun  46399  founiiun0  46410  climuzlem  46958  stirlinglem13  47301  fourierdlem112  47433  2reuimp0  48390  2reuimp  48391  gbogbow  49059  sbgoldbo  49090  iineq0  50136  iuneqconst2  50139  iineqconst2  50140  sepcsepo  50246  seppsepf  50248