Theorem reximi 3243

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3139

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  r19.29r  3255  2r19.29  3334  r19.29d2r  3335  r19.29vva  3336  r19.35  3341  r19.40  3346  2reu2rex  3432  reu3  3717  2reu5  3748  reuan  3879  ssiun  4962  iinss  4972  elsnxp  6136  elunirn  7004  iiner  8363  erovlem  8387  xpf1o  8673  unbnn2  8769  scott0  9309  dfac2b  9550  cflm  9666  alephsing  9692  numthcor  9910  zorng  9920  zornn0g  9921  ttukeyg  9933  uniimadom  9960  axgroth3  10247  qextlt  12590  qextle  12591  mptnn0fsuppd  13360  hashgt23el  13779  hash2sspr  13840  cshword  14147  rexanre  14700  climi2  14862  climi0  14863  rlimres  14909  lo1res  14910  caurcvgr  15024  caurcvg2  15028  caucvgb  15030  prodmolem2  15283  prodmo  15284  vdwnnlem1  16325  cshwsiun  16427  isnmnd  17909  efgrelexlemb  18870  nn0gsumfz0  19099  ablsimpgfind  19226  pmatcollpw2lem  21379  eltg2b  21561  neiptopuni  21732  neiptopnei  21734  ordtbas2  21793  lmcvg  21864  cnprest  21891  lmcnp  21906  nrmsep2  21958  bwth  22012  1stcfb  22047  islly2  22086  llycmpkgen  22154  txbas  22169  tx1stc  22252  cnextcn  22669  tmdcn2  22691  utoptop  22837  ucnima  22884  cfiluweak  22898  metrest  23128  metust  23162  cfilucfil  23163  metustbl  23170  xrhmeo  23544  cmetcaulem  23885  iundisj  24143  limcresi  24477  elply2  24780  aalioulem2  24916  ulmf  24964  lgamucov2  25610  2sqlem7  25994  2sqreultblem  26018  2sqreunnltblem  26021  pntrsumbnd  26136  istrkg2ld  26240  tgisline  26407  umgr2edgneu  26990  umgr3v3e3cycl  27957  eucrctshift  28016  1to3vfriendship  28054  2pthfrgrrn  28055  grpoidval  28284  grporcan  28289  grpoinveu  28290  iunrnmptss  30311  iundisjf  30333  xlt2addrd  30476  xrofsup  30486  iundisjfi  30513  rhmdvdsr  30886  tpr2rico  31150  esumc  31305  esumfsup  31324  esumpcvgval  31332  hasheuni  31339  esumiun  31348  voliune  31483  volfiniune  31484  dya2icoseg2  31531  dya2iocnei  31535  dya2iocuni  31536  omssubaddlem  31552  omssubadd  31553  afsval  31937  bnj31  31984  bnj1239  32072  bnj900  32196  bnj906  32197  bnj1398  32301  bnj1498  32328  satfvsuclem1  32601  satfv1  32605  satfvsucsuc  32607  nosupno  33198  nosupfv  33201  colinearex  33516  segcon2  33561  opnrebl2  33664  nlpfvineqsn  34684  fvineqsneq  34687  pibt2  34692  sdclem2  35011  heibor1lem  35081  grpomndo  35147  prtlem9  35994  prter1  36009  prter2  36011  hl2at  36535  cvrval4N  36544  athgt  36586  1dimN  36601  lhpexnle  37136  lhpexle1  37138  cdlemftr2  37696  cdlemftr1  37697  cdlemftr0  37698  cdlemg5  37735  cdlemg33c0  37832  mapdrvallem2  38775  eldiophb  39347  rmxyelqirr  39500  hbtlem1  39716  hbtlem7  39718  ss2iundf  39997  mnupwd  40596  iinssf  41400  founiiun  41428  founiiun0  41444  climuzlem  42017  stirlinglem13  42365  fourierdlem112  42497  2reuimp0  43307  2reuimp  43308  gbogbow  43915  sbgoldbo  43946