Theorem rspcev 2929

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823

This theorem is used by:  rspcedvdw  2936  rspceaimv  2938  rspc2ev  2945  rspc3ev  2947  rspceeqv  2948  reu6i  3017  rspesbca  3137  brralrspcev  4190  nn0suc  4753  elrnmpt1s  5034  elrnrexdm  5850  eldmrexrn  5852  foco2  5962  elabrex  5966  elabrexg  5967  f1elima  5982  fcofo  5993  fliftfun  6005  fliftval  6009  f1oiso2  6036  fo1st  6395  fo2nd  6396  tfr0dm  6598  tfrlemisucaccv  6601  tfrlemi14d  6609  tfrexlem  6610  tfr1onlemsucaccv  6617  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllemres  6638  rdgss  6659  frecabcl  6675  nnaordex  6806  nnawordex  6807  ecelqsg  6867  snfig  7109  nnfi  7180  findcard  7198  fimax2gtrilemstep  7211  unsnfi  7232  eqsupti  7342  supmaxti  7350  supisoex  7355  infminti  7373  finomni  7486  nninfwlpoimlemginf  7522  isnumi  7533  oncardval  7537  archnqq  7790  prarloclemarch2  7792  prcdnql  7857  prcunqu  7858  prarloclemlo  7867  prarloclem5  7873  nqprm  7915  1idprl  7963  1idpru  7964  ltexpri  7986  prplnqu  7993  recexprlemm  7997  recexprlem1ssl  8006  recexprlem1ssu  8007  recexpr  8011  aptiprleml  8012  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemloc  8025  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgpr  8035  caucvgprlemm  8041  caucvgprlemloc  8048  caucvgprlem1  8052  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgprpr  8085  suplocexprlemmu  8091  suplocexprlemloc  8094  suplocexpr  8098  negexsr  8145  recexgt0sr  8146  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  suplocsrlem  8181  axrnegex  8252  axprecex  8253  nntopi  8267  axcaucvglemres  8272  axpre-suploclemres  8274  cnegex  8511  recexre  8914  recexap  8989  receuap  9007  rerecapb  9181  sup3exmid  9295  cju  9299  nn2ge  9346  nominpos  9554  zdiv  9744  btwnz  9775  supinfneg  10010  infsupneg  10011  ublbneg  10028  lbzbi  10031  zq  10041  z2ge  10244  iccsupr  10384  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  zsupssdc  10689  exbtwnzlemstep  10698  exbtwnzlemex  10700  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnre  10707  qbtwnxr  10708  expnbnd  11121  hashunlem  11265  iswrdinn0  11330  shftlem  11602  shftfvalg  11604  shftfval  11607  caucvgre  11768  cvg1nlemres  11772  rexanuz  11775  rexuz3  11777  resqrexlemex  11812  caubnd2  11905  maxabslemval  11996  maxleast  12001  rexanre  12008  rexico  12009  fimaxre2  12015  minmax  12019  xrmaxiflemval  12040  xrmaxaddlem  12050  xrminmax  12055  climconst  12080  climshftlemg  12092  cn1lem  12104  serf0  12142  zsumdc  12175  fsum3  12178  fsum3cvg3  12187  mertenslemi1  12326  ntrivcvgap0  12340  zproddc  12370  fprodseq  12374  fprodntrivap  12375  dvdsval2  12581  dvds0lem  12592  dvds1lem  12593  dvds2lem  12594  odd2np1lem  12663  odd2np1  12664  opeo  12688  omeo  12689  divalglemex  12713  bezoutlemnewy  12797  bezoutlemaz  12804  bezoutlembz  12805  bezoutlemsup  12810  nnwodc  12837  uzwodc  12838  ncoprmgcdne1b  12891  exprmfct  12941  reumodprminv  13060  modprm0  13061  nnnn0modprm0  13062  pythagtriplem19  13089  pcprmpw2  13140  pockthi  13165  infpnlem2  13167  ballotfilem4  13298  ballotfilemic  13307  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemrn  13367  ennnfonelemnn0  13370  ennnfonelemim  13372  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  ctinf  13378  ctiunctlemf  13386  ismgmid2  13758  mgmidsssn0  13762  ismndd  13808  isgrpd2  13884  isgrpd  13886  imasgrp2  13971  mhmmnd  13977  ghmgrp  13979  dvdsrmuld  14511  dvdsr01  14519  rhmdvdsr  14590  lspf  14834  lspval  14835  lssats2  14859  aspval  15123  fiinbas  15292  topbas  15310  clsval  15354  neiint  15388  neipsm  15397  opnneissb  15398  opnssneib  15399  innei  15406  restbasg  15411  lmconst  15459  iscnp4  15461  cncnpi  15471  cnconst2  15476  cnptoprest  15482  cnpdis  15485  neitx  15511  txcnp  15514  blssps  15670  blss  15671  blssexps  15672  blssex  15673  ssblex  15674  blin2  15675  neibl  15734  metss2  15741  bdmopn  15747  metrest  15749  metcnp3  15754  tgioo  15797  tgqioo  15798  addcncntoplem  15804  cnopnap  15854  dedekindeulemuub  15860  suplociccreex  15867  dedekindicclemuub  15869  ivthinclemlm  15877  ivthinclemum  15878  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthreinc  15888  elply2  15978  reeff1oleme  16015  sin0pilem2  16026  sgmnncl  16274  dvdsppwf1o  16300  perfect  16318  bpos1lem  16326  bj-nn0suc0  17198  bj-inf2vnlem1  17218  3dom  17240  nninfsellemeq  17280  nninfomnilem  17284  qdencn  17295  trirec0  17317  qdiff  17322