Theorem rspcev 2907

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcev	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		nfv 1574	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2902	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∃wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801

This theorem is referenced by:  rspceaimv  2915  rspc2ev  2922  rspc3ev  2924  rspceeqv  2925  reu6i  2994  rspesbca  3114  brralrspcev  4141  nn0suc  4695  elrnmpt1s  4973  elrnrexdm  5773  eldmrexrn  5775  foco2  5876  elabrex  5880  elabrexg  5881  f1elima  5896  fcofo  5907  fliftfun  5919  fliftval  5923  f1oiso2  5950  fo1st  6301  fo2nd  6302  tfr0dm  6466  tfrlemisucaccv  6469  tfrlemi14d  6477  tfrexlem  6478  tfr1onlemsucaccv  6485  tfr1onlemres  6493  tfrcllemsucaccv  6498  tfrcllemres  6506  rdgss  6527  frecabcl  6543  nnaordex  6672  nnawordex  6673  ecelqsg  6733  snfig  6965  nnfi  7030  findcard  7046  fimax2gtrilemstep  7058  unsnfi  7077  eqsupti  7159  supmaxti  7167  supisoex  7172  infminti  7190  finomni  7303  nninfwlpoimlemginf  7339  isnumi  7350  oncardval  7354  archnqq  7600  prarloclemarch2  7602  prcdnql  7667  prcunqu  7668  prarloclemlo  7677  prarloclem5  7683  nqprm  7725  1idprl  7773  1idpru  7774  ltexpri  7796  prplnqu  7803  recexprlemm  7807  recexprlem1ssl  7816  recexprlem1ssu  7817  recexpr  7821  aptiprleml  7822  archpr  7826  cauappcvgprlemm  7828  cauappcvgprlemloc  7835  cauappcvgprlem1  7842  cauappcvgprlem2  7843  cauappcvgpr  7845  caucvgprlemm  7851  caucvgprlemloc  7858  caucvgprlem1  7862  caucvgprlem2  7863  caucvgpr  7865  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlem1  7892  caucvgprprlem2  7893  caucvgprpr  7895  suplocexprlemmu  7901  suplocexprlemloc  7904  suplocexpr  7908  negexsr  7955  recexgt0sr  7956  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  suplocsrlem  7991  axrnegex  8062  axprecex  8063  nntopi  8077  axcaucvglemres  8082  axpre-suploclemres  8084  cnegex  8320  recexre  8721  recexap  8796  receuap  8812  rerecapb  8986  sup3exmid  9100  cju  9104  nn2ge  9139  nominpos  9345  zdiv  9531  btwnz  9562  supinfneg  9786  infsupneg  9787  ublbneg  9804  lbzbi  9807  zq  9817  z2ge  10018  iccsupr  10158  zsupcllemstep  10444  infssuzex  10448  suprzubdc  10451  zsupssdc  10453  exbtwnzlemstep  10462  exbtwnzlemex  10464  rebtwn2zlemstep  10467  rebtwn2z  10469  qbtwnre  10471  qbtwnxr  10472  expnbnd  10880  hashunlem  11021  iswrdinn0  11071  shftlem  11322  shftfvalg  11324  shftfval  11327  caucvgre  11487  cvg1nlemres  11491  rexanuz  11494  rexuz3  11496  resqrexlemex  11531  caubnd2  11623  maxabslemval  11714  maxleast  11719  rexanre  11726  rexico  11727  fimaxre2  11733  minmax  11736  xrmaxiflemval  11756  xrmaxaddlem  11766  xrminmax  11771  climconst  11796  climshftlemg  11808  cn1lem  11820  serf0  11858  zsumdc  11890  fsum3  11893  fsum3cvg3  11902  mertenslemi1  12041  ntrivcvgap0  12055  zproddc  12085  fprodseq  12089  fprodntrivap  12090  dvdsval2  12296  dvds0lem  12307  dvds1lem  12308  dvds2lem  12309  odd2np1lem  12378  odd2np1  12379  opeo  12403  omeo  12404  divalglemex  12428  bezoutlemnewy  12512  bezoutlemaz  12519  bezoutlembz  12520  bezoutlemsup  12525  nnwodc  12552  uzwodc  12553  ncoprmgcdne1b  12606  exprmfct  12655  reumodprminv  12771  modprm0  12772  nnnn0modprm0  12773  pythagtriplem19  12800  pcprmpw2  12851  pockthi  12876  infpnlem2  12878  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemrn  12985  ennnfonelemnn0  12988  ennnfonelemim  12990  exmidunben  12992  ctinfomlemom  12993  ctinfom  12994  ctinf  12996  ctiunctlemf  13004  ismgmid2  13408  mgmidsssn0  13412  ismndd  13465  isgrpd2  13549  isgrpd  13551  imasgrp2  13642  mhmmnd  13648  ghmgrp  13650  dvdsrmuld  14054  dvdsr01  14062  rhmdvdsr  14133  lspf  14347  lspval  14348  lssats2  14372  fiinbas  14717  topbas  14735  clsval  14779  neiint  14813  neipsm  14822  opnneissb  14823  opnssneib  14824  innei  14831  restbasg  14836  lmconst  14884  iscnp4  14886  cncnpi  14896  cnconst2  14901  cnptoprest  14907  cnpdis  14910  neitx  14936  txcnp  14939  blssps  15095  blss  15096  blssexps  15097  blssex  15098  ssblex  15099  blin2  15100  neibl  15159  metss2  15166  bdmopn  15172  metrest  15174  metcnp3  15179  tgioo  15222  tgqioo  15223  addcncntoplem  15229  cnopnap  15279  dedekindeulemuub  15285  suplociccreex  15292  dedekindicclemuub  15294  ivthinclemlm  15302  ivthinclemum  15303  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthreinc  15313  elply2  15403  reeff1oleme  15440  sin0pilem2  15450  sgmnncl  15656  dvdsppwf1o  15657  perfect  15669  bj-nn0suc0  16271  bj-inf2vnlem1  16291  nninfsellemeq  16339  nninfomnilem  16343  qdencn  16354  trirec0  16371