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 2145  ∃wrex 3088

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 3089

This theorem is used by:  r19.35  3122  r19.40  3130  2r19.29  3150  2reu2rex  3379  reu3  3688  2reu5  3719  reuan  3847  dfiun2g  4992  ssiun  5009  iinss  5019  elsnxp  6293  elunirn  7251  el2xpss  8037  iiner  8792  erovlem  8816  xpf1o  9140  enp1i  9252  unbnn2  9270  scott0b  9879  scott0OLD  9880  dfac2b  10136  cflm  10254  alephsing  10281  numthcor  10499  zorng  10509  zornn0g  10510  ttukeyg  10522  uniimadom  10555  axgroth3  10843  qextlt  13257  qextle  13258  mptnn0fsuppd  14064  hashgt23el  14491  hash2sspr  14556  cshword  14864  rexanre  15436  climi2  15600  climi0  15601  rlimres  15647  lo1res  15648  caurcvgr  15763  caurcvg2  15767  caucvgb  15769  prodmolem2  16026  prodmo  16027  vdwnnlem1  17091  cshwsiun  17195  isnmnd  18844  efgrelexlemb  19881  nn0gsumfz0  20116  ablsimpgfind  20243  rhmdvdsr  20672  isdrng4  20906  pmatcollpw2lem  23006  eltg2b  23188  neiptopuni  23359  neiptopnei  23361  ordtbas2  23420  lmcvg  23491  cnprest  23518  lmcnp  23533  nrmsep2  23585  bwth  23639  1stcfb  23674  islly2  23714  llycmpkgen  23782  txbas  23797  tx1stc  23880  cnextcn  24297  tmdcn2  24319  utoptop  24464  ucnima  24510  cfiluweak  24524  metrest  24754  metust  24788  cfilucfil  24789  metustbl  24796  xrhmeo  25178  cmetcaulem  25520  iundisj  25780  limcresi  26117  elply2  26426  aalioulem2  26569  ulmf  26618  lgamucov2  27276  2sqlem7  27661  2sqreultblem  27685  2sqreunnltblem  27688  pntrsumbnd  27803  nosupno  27940  nosupfv  27943  noinfno  27955  noinffv  27958  istrkg2ld  28802  tgisline  28975  cgrabasimass  29258  umgr2edgneu  29675  umgr3v3e3cycl  30665  eucrctshift  30724  1to3vfriendship  30762  2pthfrgrrn  30763  grpoidval  30995  grporcan  31000  grpoinveu  31001  iunrnmptss  33040  iundisjf  33064  xlt2addrd  33232  xrofsup  33240  iundisjfi  33269  dflringlem2  33907  tpr2rico  34424  esumc  34563  esumfsup  34582  esumpcvgval  34590  hasheuni  34597  esumiun  34606  voliune  34742  volfiniune  34743  dya2icoseg2  34791  dya2iocnei  34795  dya2iocuni  34796  omssubaddlem  34812  omssubadd  34813  afsval  35184  bnj31  35231  bnj1239  35316  bnj900  35440  bnj906  35441  bnj1398  35545  bnj1498  35572  nummin  35600  r1omhf  35616  noinfepregs  35661  onvf1odlem1  35702  vonf1oonfo  35714  satfvsuclem1  35940  satfv1  35944  satfvsucsuc  35946  colinearex  36642  segcon2  36687  opnrebl2  36942  regsfromunir1  37161  nlpfvineqsn  38165  fvineqsneq  38168  pibt2  38173  sdclem2  38494  heibor1lem  38561  grpomndo  38627  disjdmqsss  39655  disjdmqscossss  39656  dmqsblocks  39717  prtlem9  39739  prter1  39754  prter2  39756  hl2at  40280  cvrval4N  40289  athgt  40331  1dimN  40346  lhpexnle  40881  lhpexle1  40883  cdlemftr2  41441  cdlemftr1  41442  cdlemftr0  41443  cdlemg5  41480  cdlemg33c0  41577  mapdrvallem2  42520  sn-negex  43295  sn-negex2  43296  eldiophb  43604  rmxyelqirr  43753  hbtlem1  43966  hbtlem7  43968  ss2iundf  44501  mnupwd  45093  ismnushort  45127  iinssf  45972  founiiun  46013  founiiun0  46024  climuzlem  46573  stirlinglem13  46916  fourierdlem112  47048  2reuimp0  48004  2reuimp  48005  gbogbow  48674  sbgoldbo  48705  iineq0  49750  iuneqconst2  49753  iineqconst2  49754  sepcsepo  49855  seppsepf  49857