Theorem reximi 3067

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.35  3088  r19.35OLD  3089  r19.29rOLD  3097  r19.40  3099  2r19.29  3119  2reu2rex  3368  reu3  3698  2reu5  3729  reuan  3859  dfiun2g  4994  ssiun  5010  iinss  5020  elsnxp  6264  elunirn  7225  el2xpss  8016  iiner  8762  erovlem  8786  xpf1o  9103  enp1i  9224  unbnn2  9244  scott0  9839  dfac2b  10084  cflm  10203  alephsing  10229  numthcor  10447  zorng  10457  zornn0g  10458  ttukeyg  10470  uniimadom  10497  axgroth3  10784  qextlt  13163  qextle  13164  mptnn0fsuppd  13963  hashgt23el  14389  hash2sspr  14454  cshword  14756  rexanre  15313  climi2  15477  climi0  15478  rlimres  15524  lo1res  15525  caurcvgr  15640  caurcvg2  15644  caucvgb  15646  prodmolem2  15901  prodmo  15902  vdwnnlem1  16966  cshwsiun  17070  isnmnd  18665  efgrelexlemb  19680  nn0gsumfz0  19915  ablsimpgfind  20042  rhmdvdsr  20417  pmatcollpw2lem  22664  eltg2b  22846  neiptopuni  23017  neiptopnei  23019  ordtbas2  23078  lmcvg  23149  cnprest  23176  lmcnp  23191  nrmsep2  23243  bwth  23297  1stcfb  23332  islly2  23371  llycmpkgen  23439  txbas  23454  tx1stc  23537  cnextcn  23954  tmdcn2  23976  utoptop  24122  ucnima  24168  cfiluweak  24182  metrest  24412  metust  24446  cfilucfil  24447  metustbl  24454  xrhmeo  24844  cmetcaulem  25188  iundisj  25449  limcresi  25786  elply2  26101  aalioulem2  26241  ulmf  26291  lgamucov2  26949  2sqlem7  27335  2sqreultblem  27359  2sqreunnltblem  27362  pntrsumbnd  27477  nosupno  27615  nosupfv  27618  noinfno  27630  noinffv  27633  istrkg2ld  28387  tgisline  28554  umgr2edgneu  29141  umgr3v3e3cycl  30113  eucrctshift  30172  1to3vfriendship  30210  2pthfrgrrn  30211  grpoidval  30442  grporcan  30447  grpoinveu  30448  iunrnmptss  32494  iundisjf  32518  xlt2addrd  32682  xrofsup  32690  iundisjfi  32719  isdrng4  33245  tpr2rico  33902  esumc  34041  esumfsup  34060  esumpcvgval  34068  hasheuni  34075  esumiun  34084  voliune  34219  volfiniune  34220  dya2icoseg2  34269  dya2iocnei  34273  dya2iocuni  34274  omssubaddlem  34290  omssubadd  34291  afsval  34662  bnj31  34709  bnj1239  34795  bnj900  34919  bnj906  34920  bnj1398  35024  bnj1498  35051  nummin  35081  onvf1odlem1  35090  satfvsuclem1  35346  satfv1  35350  satfvsucsuc  35352  colinearex  36048  segcon2  36093  opnrebl2  36309  nlpfvineqsn  37397  fvineqsneq  37400  pibt2  37405  sdclem2  37736  heibor1lem  37803  grpomndo  37869  disjdmqsss  38794  disjdmqscossss  38795  dmqsblocks  38845  prtlem9  38857  prter1  38872  prter2  38874  hl2at  39399  cvrval4N  39408  athgt  39450  1dimN  39465  lhpexnle  40000  lhpexle1  40002  cdlemftr2  40560  cdlemftr1  40561  cdlemftr0  40562  cdlemg5  40599  cdlemg33c0  40696  mapdrvallem2  41639  sn-negex  42406  sn-negex2  42407  eldiophb  42745  rmxyelqirr  42898  rmxyelqirrOLD  42899  hbtlem1  43112  hbtlem7  43114  ss2iundf  43648  mnupwd  44256  ismnushort  44290  iinssf  45132  founiiun  45173  founiiun0  45184  climuzlem  45741  stirlinglem13  46084  fourierdlem112  46216  2reuimp0  47115  2reuimp  47116  gbogbow  47757  sbgoldbo  47788  iineq0  48808  iuneqconst2  48811  iineqconst2  48812  sepcsepo  48915  seppsepf  48917