Theorem rspcev 2876

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 1550	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2871	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372   ∈ wcel 2175  ∃wrex 2484

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773

This theorem is referenced by:  rspceaimv  2884  rspc2ev  2891  rspc3ev  2893  rspceeqv  2894  reu6i  2963  rspesbca  3082  brralrspcev  4101  nn0suc  4651  elrnmpt1s  4927  elrnrexdm  5718  eldmrexrn  5720  foco2  5821  elabrex  5825  elabrexg  5826  f1elima  5841  fcofo  5852  fliftfun  5864  fliftval  5868  f1oiso2  5895  fo1st  6242  fo2nd  6243  tfr0dm  6407  tfrlemisucaccv  6410  tfrlemi14d  6418  tfrexlem  6419  tfr1onlemsucaccv  6426  tfr1onlemres  6434  tfrcllemsucaccv  6439  tfrcllemres  6447  rdgss  6468  frecabcl  6484  nnaordex  6613  nnawordex  6614  ecelqsg  6674  snfig  6905  nnfi  6968  findcard  6984  fimax2gtrilemstep  6996  unsnfi  7015  eqsupti  7097  supmaxti  7105  supisoex  7110  infminti  7128  finomni  7241  nninfwlpoimlemginf  7277  isnumi  7288  oncardval  7292  archnqq  7529  prarloclemarch2  7531  prcdnql  7596  prcunqu  7597  prarloclemlo  7606  prarloclem5  7612  nqprm  7654  1idprl  7702  1idpru  7703  ltexpri  7725  prplnqu  7732  recexprlemm  7736  recexprlem1ssl  7745  recexprlem1ssu  7746  recexpr  7750  aptiprleml  7751  archpr  7755  cauappcvgprlemm  7757  cauappcvgprlemloc  7764  cauappcvgprlem1  7771  cauappcvgprlem2  7772  cauappcvgpr  7774  caucvgprlemm  7780  caucvgprlemloc  7787  caucvgprlem1  7791  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgprpr  7824  suplocexprlemmu  7830  suplocexprlemloc  7833  suplocexpr  7837  negexsr  7884  recexgt0sr  7885  caucvgsrlemgt1  7907  caucvgsrlemoffres  7912  suplocsrlem  7920  axrnegex  7991  axprecex  7992  nntopi  8006  axcaucvglemres  8011  axpre-suploclemres  8013  cnegex  8249  recexre  8650  recexap  8725  receuap  8741  rerecapb  8915  sup3exmid  9029  cju  9033  nn2ge  9068  nominpos  9274  zdiv  9460  btwnz  9491  supinfneg  9715  infsupneg  9716  ublbneg  9733  lbzbi  9736  zq  9746  z2ge  9947  iccsupr  10087  zsupcllemstep  10370  infssuzex  10374  suprzubdc  10377  zsupssdc  10379  exbtwnzlemstep  10388  exbtwnzlemex  10390  rebtwn2zlemstep  10393  rebtwn2z  10395  qbtwnre  10397  qbtwnxr  10398  expnbnd  10806  hashunlem  10947  iswrdinn0  10997  shftlem  11069  shftfvalg  11071  shftfval  11074  caucvgre  11234  cvg1nlemres  11238  rexanuz  11241  rexuz3  11243  resqrexlemex  11278  caubnd2  11370  maxabslemval  11461  maxleast  11466  rexanre  11473  rexico  11474  fimaxre2  11480  minmax  11483  xrmaxiflemval  11503  xrmaxaddlem  11513  xrminmax  11518  climconst  11543  climshftlemg  11555  cn1lem  11567  serf0  11605  zsumdc  11637  fsum3  11640  fsum3cvg3  11649  mertenslemi1  11788  ntrivcvgap0  11802  zproddc  11832  fprodseq  11836  fprodntrivap  11837  dvdsval2  12043  dvds0lem  12054  dvds1lem  12055  dvds2lem  12056  odd2np1lem  12125  odd2np1  12126  opeo  12150  omeo  12151  divalglemex  12175  bezoutlemnewy  12259  bezoutlemaz  12266  bezoutlembz  12267  bezoutlemsup  12272  nnwodc  12299  uzwodc  12300  ncoprmgcdne1b  12353  exprmfct  12402  reumodprminv  12518  modprm0  12519  nnnn0modprm0  12520  pythagtriplem19  12547  pcprmpw2  12598  pockthi  12623  infpnlem2  12625  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemrn  12732  ennnfonelemnn0  12735  ennnfonelemim  12737  exmidunben  12739  ctinfomlemom  12740  ctinfom  12741  ctinf  12743  ctiunctlemf  12751  ismgmid2  13154  mgmidsssn0  13158  ismndd  13211  isgrpd2  13295  isgrpd  13297  imasgrp2  13388  mhmmnd  13394  ghmgrp  13396  dvdsrmuld  13800  dvdsr01  13808  rhmdvdsr  13879  lspf  14093  lspval  14094  lssats2  14118  fiinbas  14463  topbas  14481  clsval  14525  neiint  14559  neipsm  14568  opnneissb  14569  opnssneib  14570  innei  14577  restbasg  14582  lmconst  14630  iscnp4  14632  cncnpi  14642  cnconst2  14647  cnptoprest  14653  cnpdis  14656  neitx  14682  txcnp  14685  blssps  14841  blss  14842  blssexps  14843  blssex  14844  ssblex  14845  blin2  14846  neibl  14905  metss2  14912  bdmopn  14918  metrest  14920  metcnp3  14925  tgioo  14968  tgqioo  14969  addcncntoplem  14975  cnopnap  15025  dedekindeulemuub  15031  suplociccreex  15038  dedekindicclemuub  15040  ivthinclemlm  15048  ivthinclemum  15049  ivthinclemlopn  15050  ivthinclemuopn  15052  ivthreinc  15059  elply2  15149  reeff1oleme  15186  sin0pilem2  15196  sgmnncl  15402  dvdsppwf1o  15403  perfect  15415  bj-nn0suc0  15819  bj-inf2vnlem1  15839  nninfsellemeq  15884  nninfomnilem  15888  qdencn  15899  trirec0  15916