Theorem reximi 3156

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
reximi	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	reximia 3155	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2112  ∃wrex 3052

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3056  df-rex 3057

This theorem is referenced by:  r19.29r  3167  2r19.29  3240  r19.29d2r  3241  r19.29vva  3242  r19.35  3245  r19.40  3249  2reu2rex  3329  reu3  3629  2reu5  3660  reuan  3795  ssiun  4941  iinss  4951  elsnxp  6134  elunirn  7042  iiner  8449  erovlem  8473  xpf1o  8786  unbnn2  8906  scott0  9467  dfac2b  9709  cflm  9829  alephsing  9855  numthcor  10073  zorng  10083  zornn0g  10084  ttukeyg  10096  uniimadom  10123  axgroth3  10410  qextlt  12758  qextle  12759  mptnn0fsuppd  13536  hashgt23el  13956  hash2sspr  14019  cshword  14321  rexanre  14875  climi2  15037  climi0  15038  rlimres  15084  lo1res  15085  caurcvgr  15202  caurcvg2  15206  caucvgb  15208  prodmolem2  15460  prodmo  15461  vdwnnlem1  16511  cshwsiun  16616  isnmnd  18131  efgrelexlemb  19094  nn0gsumfz0  19324  ablsimpgfind  19451  pmatcollpw2lem  21628  eltg2b  21810  neiptopuni  21981  neiptopnei  21983  ordtbas2  22042  lmcvg  22113  cnprest  22140  lmcnp  22155  nrmsep2  22207  bwth  22261  1stcfb  22296  islly2  22335  llycmpkgen  22403  txbas  22418  tx1stc  22501  cnextcn  22918  tmdcn2  22940  utoptop  23086  ucnima  23132  cfiluweak  23146  metrest  23376  metust  23410  cfilucfil  23411  metustbl  23418  xrhmeo  23797  cmetcaulem  24139  iundisj  24399  limcresi  24736  elply2  25044  aalioulem2  25180  ulmf  25228  lgamucov2  25875  2sqlem7  26259  2sqreultblem  26283  2sqreunnltblem  26286  pntrsumbnd  26401  istrkg2ld  26505  tgisline  26672  umgr2edgneu  27256  umgr3v3e3cycl  28221  eucrctshift  28280  1to3vfriendship  28318  2pthfrgrrn  28319  grpoidval  28548  grporcan  28553  grpoinveu  28554  iunrnmptss  30578  iundisjf  30601  xlt2addrd  30755  xrofsup  30764  iundisjfi  30791  rhmdvdsr  31190  tpr2rico  31530  esumc  31685  esumfsup  31704  esumpcvgval  31712  hasheuni  31719  esumiun  31728  voliune  31863  volfiniune  31864  dya2icoseg2  31911  dya2iocnei  31915  dya2iocuni  31916  omssubaddlem  31932  omssubadd  31933  afsval  32317  bnj31  32364  bnj1239  32452  bnj900  32576  bnj906  32577  bnj1398  32681  bnj1498  32708  nummin  32730  satfvsuclem1  32988  satfv1  32992  satfvsucsuc  32994  elxpxpss  33354  nosupno  33592  nosupfv  33595  noinfno  33607  noinffv  33610  colinearex  34048  segcon2  34093  opnrebl2  34196  nlpfvineqsn  35266  fvineqsneq  35269  pibt2  35274  sdclem2  35586  heibor1lem  35653  grpomndo  35719  prtlem9  36564  prter1  36579  prter2  36581  hl2at  37105  cvrval4N  37114  athgt  37156  1dimN  37171  lhpexnle  37706  lhpexle1  37708  cdlemftr2  38266  cdlemftr1  38267  cdlemftr0  38268  cdlemg5  38305  cdlemg33c0  38402  mapdrvallem2  39345  sn-negex  40048  sn-negex2  40049  eldiophb  40223  rmxyelqirr  40376  hbtlem1  40592  hbtlem7  40594  ss2iundf  40885  mnupwd  41499  ismnushort  41533  iinssf  42301  founiiun  42329  founiiun0  42342  climuzlem  42902  stirlinglem13  43245  fourierdlem112  43377  2reuimp0  44221  2reuimp  44222  gbogbow  44824  sbgoldbo  44855  sepcsepo  45836  seppsepf  45838