Theorem reximi 3011

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  2r19.29  3079  r19.29d2r  3080  r19.40  3088  reu3  3396  2reu5  3416  ssiun  4562  iinss  4571  elsnxp  5677  elsnxpOLD  5678  elunirn  6509  iiner  7819  erovlem  7843  xpf1o  8122  unbnn2  8217  scott0  8749  dfac2  8953  cflm  9072  alephsing  9098  numthcor  9316  zorng  9326  zornn0g  9327  ttukeyg  9339  uniimadom  9366  axgroth3  9653  qextlt  12034  qextle  12035  mptnn0fsuppd  12798  hash2sspr  13270  cshword  13537  rexanre  14086  climi2  14242  climi0  14243  rlimres  14289  lo1res  14290  caurcvgr  14404  caurcvg2  14408  caucvgb  14410  prodmolem2  14665  prodmo  14666  vdwnnlem1  15699  cshwsiun  15806  isnmnd  17298  efgrelexlemb  18163  nn0gsumfz0  18381  pmatcollpw2lem  20582  eltg2b  20763  neiptopuni  20934  neiptopnei  20936  ordtbas2  20995  lmcvg  21066  cnprest  21093  lmcnp  21108  nrmsep2  21160  bwth  21213  1stcfb  21248  islly2  21287  llycmpkgen  21355  txbas  21370  tx1stc  21453  cnextcn  21871  tmdcn2  21893  utoptop  22038  ucnima  22085  cfiluweak  22099  metrest  22329  metust  22363  cfilucfil  22364  metustbl  22371  xrhmeo  22745  cmetcaulem  23086  iundisj  23316  limcresi  23649  elply2  23952  aalioulem2  24088  ulmf  24136  lgamucov2  24765  2sqlem7  25149  pntrsumbnd  25255  istrkg2ld  25359  tgisline  25522  umgr2edgneu  26106  umgr3v3e3cycl  27044  eucrctshift  27103  1to3vfriendship  27145  2pthfrgrrn  27146  grpoidval  27367  grporcan  27372  grpoinveu  27373  iundisjf  29402  xlt2addrd  29523  xrofsup  29533  iundisjfi  29555  rhmdvdsr  29818  tpr2rico  29958  esumc  30113  esumfsup  30132  esumpcvgval  30140  hasheuni  30147  esumiun  30156  voliune  30292  volfiniune  30293  dya2icoseg2  30340  dya2iocnei  30344  dya2iocuni  30345  omssubaddlem  30361  omssubadd  30362  afsval  30749  bnj31  30785  bnj1239  30876  bnj900  30999  bnj906  31000  bnj1398  31102  bnj1498  31129  nosupno  31849  nosupfv  31852  colinearex  32167  segcon2  32212  opnrebl2  32316  sdclem2  33538  heibor1lem  33608  grpomndo  33674  prtlem9  34149  prtlem11  34151  prter1  34164  prter2  34166  hl2at  34691  cvrval4N  34700  athgt  34742  1dimN  34757  lhpexnle  35292  lhpexle1  35294  cdlemftr2  35854  cdlemftr1  35855  cdlemftr0  35856  cdlemg5  35893  cdlemg33c0  35990  mapdrvallem2  36934  eldiophb  37320  rmxyelqirr  37475  hbtlem1  37693  hbtlem7  37695  ss2iundf  37951  iinssf  39327  founiiun  39360  founiiun0  39377  climuzlem  39975  stirlinglem13  40303  fourierdlem112  40435  reuan  41180  2reu2rex  41183  cshword2  41437  gbogbow  41644  sbgoldbo  41675