Theorem rspcev 2908

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 2903	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 2802

This theorem is referenced by:  rspceaimv  2916  rspc2ev  2923  rspc3ev  2925  rspceeqv  2926  reu6i  2995  rspesbca  3115  brralrspcev  4145  nn0suc  4700  elrnmpt1s  4980  elrnrexdm  5782  eldmrexrn  5784  foco2  5889  elabrex  5893  elabrexg  5894  f1elima  5909  fcofo  5920  fliftfun  5932  fliftval  5936  f1oiso2  5963  fo1st  6315  fo2nd  6316  tfr0dm  6483  tfrlemisucaccv  6486  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemsucaccv  6502  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllemres  6523  rdgss  6544  frecabcl  6560  nnaordex  6691  nnawordex  6692  ecelqsg  6752  snfig  6984  nnfi  7054  findcard  7070  fimax2gtrilemstep  7083  unsnfi  7104  eqsupti  7186  supmaxti  7194  supisoex  7199  infminti  7217  finomni  7330  nninfwlpoimlemginf  7366  isnumi  7377  oncardval  7381  archnqq  7627  prarloclemarch2  7629  prcdnql  7694  prcunqu  7695  prarloclemlo  7704  prarloclem5  7710  nqprm  7752  1idprl  7800  1idpru  7801  ltexpri  7823  prplnqu  7830  recexprlemm  7834  recexprlem1ssl  7843  recexprlem1ssu  7844  recexpr  7848  aptiprleml  7849  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemloc  7862  cauappcvgprlem1  7869  cauappcvgprlem2  7870  cauappcvgpr  7872  caucvgprlemm  7878  caucvgprlemloc  7885  caucvgprlem1  7889  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgprpr  7922  suplocexprlemmu  7928  suplocexprlemloc  7931  suplocexpr  7935  negexsr  7982  recexgt0sr  7983  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  suplocsrlem  8018  axrnegex  8089  axprecex  8090  nntopi  8104  axcaucvglemres  8109  axpre-suploclemres  8111  cnegex  8347  recexre  8748  recexap  8823  receuap  8839  rerecapb  9013  sup3exmid  9127  cju  9131  nn2ge  9166  nominpos  9372  zdiv  9558  btwnz  9589  supinfneg  9819  infsupneg  9820  ublbneg  9837  lbzbi  9840  zq  9850  z2ge  10051  iccsupr  10191  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  zsupssdc  10488  exbtwnzlemstep  10497  exbtwnzlemex  10499  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnre  10506  qbtwnxr  10507  expnbnd  10915  hashunlem  11057  iswrdinn0  11108  shftlem  11367  shftfvalg  11369  shftfval  11372  caucvgre  11532  cvg1nlemres  11536  rexanuz  11539  rexuz3  11541  resqrexlemex  11576  caubnd2  11668  maxabslemval  11759  maxleast  11764  rexanre  11771  rexico  11772  fimaxre2  11778  minmax  11781  xrmaxiflemval  11801  xrmaxaddlem  11811  xrminmax  11816  climconst  11841  climshftlemg  11853  cn1lem  11865  serf0  11903  zsumdc  11935  fsum3  11938  fsum3cvg3  11947  mertenslemi1  12086  ntrivcvgap0  12100  zproddc  12130  fprodseq  12134  fprodntrivap  12135  dvdsval2  12341  dvds0lem  12352  dvds1lem  12353  dvds2lem  12354  odd2np1lem  12423  odd2np1  12424  opeo  12448  omeo  12449  divalglemex  12473  bezoutlemnewy  12557  bezoutlemaz  12564  bezoutlembz  12565  bezoutlemsup  12570  nnwodc  12597  uzwodc  12598  ncoprmgcdne1b  12651  exprmfct  12700  reumodprminv  12816  modprm0  12817  nnnn0modprm0  12818  pythagtriplem19  12845  pcprmpw2  12896  pockthi  12921  infpnlem2  12923  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemrn  13030  ennnfonelemnn0  13033  ennnfonelemim  13035  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  ctinf  13041  ctiunctlemf  13049  ismgmid2  13453  mgmidsssn0  13457  ismndd  13510  isgrpd2  13594  isgrpd  13596  imasgrp2  13687  mhmmnd  13693  ghmgrp  13695  dvdsrmuld  14100  dvdsr01  14108  rhmdvdsr  14179  lspf  14393  lspval  14394  lssats2  14418  fiinbas  14763  topbas  14781  clsval  14825  neiint  14859  neipsm  14868  opnneissb  14869  opnssneib  14870  innei  14877  restbasg  14882  lmconst  14930  iscnp4  14932  cncnpi  14942  cnconst2  14947  cnptoprest  14953  cnpdis  14956  neitx  14982  txcnp  14985  blssps  15141  blss  15142  blssexps  15143  blssex  15144  ssblex  15145  blin2  15146  neibl  15205  metss2  15212  bdmopn  15218  metrest  15220  metcnp3  15225  tgioo  15268  tgqioo  15269  addcncntoplem  15275  cnopnap  15325  dedekindeulemuub  15331  suplociccreex  15338  dedekindicclemuub  15340  ivthinclemlm  15348  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthreinc  15359  elply2  15449  reeff1oleme  15486  sin0pilem2  15496  sgmnncl  15702  dvdsppwf1o  15703  perfect  15715  bj-nn0suc0  16481  bj-inf2vnlem1  16501  3dom  16523  nninfsellemeq  16552  nninfomnilem  16556  qdencn  16567  trirec0  16584