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  11098  shftfvalg  11100  shftfval  11103  caucvgre  11263  cvg1nlemres  11267  rexanuz  11270  rexuz3  11272  resqrexlemex  11307  caubnd2  11399  maxabslemval  11490  maxleast  11495  rexanre  11502  rexico  11503  fimaxre2  11509  minmax  11512  xrmaxiflemval  11532  xrmaxaddlem  11542  xrminmax  11547  climconst  11572  climshftlemg  11584  cn1lem  11596  serf0  11634  zsumdc  11666  fsum3  11669  fsum3cvg3  11678  mertenslemi1  11817  ntrivcvgap0  11831  zproddc  11861  fprodseq  11865  fprodntrivap  11866  dvdsval2  12072  dvds0lem  12083  dvds1lem  12084  dvds2lem  12085  odd2np1lem  12154  odd2np1  12155  opeo  12179  omeo  12180  divalglemex  12204  bezoutlemnewy  12288  bezoutlemaz  12295  bezoutlembz  12296  bezoutlemsup  12301  nnwodc  12328  uzwodc  12329  ncoprmgcdne1b  12382  exprmfct  12431  reumodprminv  12547  modprm0  12548  nnnn0modprm0  12549  pythagtriplem19  12576  pcprmpw2  12627  pockthi  12652  infpnlem2  12654  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemrn  12761  ennnfonelemnn0  12764  ennnfonelemim  12766  exmidunben  12768  ctinfomlemom  12769  ctinfom  12770  ctinf  12772  ctiunctlemf  12780  ismgmid2  13183  mgmidsssn0  13187  ismndd  13240  isgrpd2  13324  isgrpd  13326  imasgrp2  13417  mhmmnd  13423  ghmgrp  13425  dvdsrmuld  13829  dvdsr01  13837  rhmdvdsr  13908  lspf  14122  lspval  14123  lssats2  14147  fiinbas  14492  topbas  14510  clsval  14554  neiint  14588  neipsm  14597  opnneissb  14598  opnssneib  14599  innei  14606  restbasg  14611  lmconst  14659  iscnp4  14661  cncnpi  14671  cnconst2  14676  cnptoprest  14682  cnpdis  14685  neitx  14711  txcnp  14714  blssps  14870  blss  14871  blssexps  14872  blssex  14873  ssblex  14874  blin2  14875  neibl  14934  metss2  14941  bdmopn  14947  metrest  14949  metcnp3  14954  tgioo  14997  tgqioo  14998  addcncntoplem  15004  cnopnap  15054  dedekindeulemuub  15060  suplociccreex  15067  dedekindicclemuub  15069  ivthinclemlm  15077  ivthinclemum  15078  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthreinc  15088  elply2  15178  reeff1oleme  15215  sin0pilem2  15225  sgmnncl  15431  dvdsppwf1o  15432  perfect  15444  bj-nn0suc0  15848  bj-inf2vnlem1  15868  nninfsellemeq  15913  nninfomnilem  15917  qdencn  15928  trirec0  15945