Theorem rspcev 2923

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2205  ∃wrex 2523

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817

This theorem is referenced by:  rspcedvdw  2930  rspceaimv  2932  rspc2ev  2939  rspc3ev  2941  rspceeqv  2942  reu6i  3011  rspesbca  3131  brralrspcev  4174  nn0suc  4733  elrnmpt1s  5014  elrnrexdm  5823  eldmrexrn  5825  foco2  5934  elabrex  5938  elabrexg  5939  f1elima  5954  fcofo  5965  fliftfun  5977  fliftval  5981  f1oiso2  6008  fo1st  6366  fo2nd  6367  tfr0dm  6568  tfrlemisucaccv  6571  tfrlemi14d  6579  tfrexlem  6580  tfr1onlemsucaccv  6587  tfr1onlemres  6595  tfrcllemsucaccv  6600  tfrcllemres  6608  rdgss  6629  frecabcl  6645  nnaordex  6776  nnawordex  6777  ecelqsg  6837  snfig  7071  nnfi  7142  findcard  7160  fimax2gtrilemstep  7173  unsnfi  7194  eqsupti  7302  supmaxti  7310  supisoex  7315  infminti  7333  finomni  7446  nninfwlpoimlemginf  7482  isnumi  7493  oncardval  7497  archnqq  7750  prarloclemarch2  7752  prcdnql  7817  prcunqu  7818  prarloclemlo  7827  prarloclem5  7833  nqprm  7875  1idprl  7923  1idpru  7924  ltexpri  7946  prplnqu  7953  recexprlemm  7957  recexprlem1ssl  7966  recexprlem1ssu  7967  recexpr  7971  aptiprleml  7972  archpr  7976  cauappcvgprlemm  7978  cauappcvgprlemloc  7985  cauappcvgprlem1  7992  cauappcvgprlem2  7993  cauappcvgpr  7995  caucvgprlemm  8001  caucvgprlemloc  8008  caucvgprlem1  8012  caucvgprlem2  8013  caucvgpr  8015  caucvgprprlemmu  8028  caucvgprprlemopl  8030  caucvgprprlemopu  8032  caucvgprprlemloc  8036  caucvgprprlem1  8042  caucvgprprlem2  8043  caucvgprpr  8045  suplocexprlemmu  8051  suplocexprlemloc  8054  suplocexpr  8058  negexsr  8105  recexgt0sr  8106  caucvgsrlemgt1  8128  caucvgsrlemoffres  8133  suplocsrlem  8141  axrnegex  8212  axprecex  8213  nntopi  8227  axcaucvglemres  8232  axpre-suploclemres  8234  cnegex  8470  recexre  8872  recexap  8947  receuap  8965  rerecapb  9139  sup3exmid  9253  cju  9257  nn2ge  9292  nominpos  9498  zdiv  9689  btwnz  9720  supinfneg  9950  infsupneg  9951  ublbneg  9968  lbzbi  9971  zq  9981  z2ge  10183  iccsupr  10323  zsupcllemstep  10616  infssuzex  10620  suprzubdc  10625  zsupssdc  10627  exbtwnzlemstep  10636  exbtwnzlemex  10638  rebtwn2zlemstep  10641  rebtwn2z  10643  qbtwnre  10645  qbtwnxr  10646  expnbnd  11055  hashunlem  11198  iswrdinn0  11259  shftlem  11531  shftfvalg  11533  shftfval  11536  caucvgre  11697  cvg1nlemres  11701  rexanuz  11704  rexuz3  11706  resqrexlemex  11741  caubnd2  11833  maxabslemval  11924  maxleast  11929  rexanre  11936  rexico  11937  fimaxre2  11943  minmax  11946  xrmaxiflemval  11966  xrmaxaddlem  11976  xrminmax  11981  climconst  12006  climshftlemg  12018  cn1lem  12030  serf0  12068  zsumdc  12101  fsum3  12104  fsum3cvg3  12113  mertenslemi1  12252  ntrivcvgap0  12266  zproddc  12296  fprodseq  12300  fprodntrivap  12301  dvdsval2  12507  dvds0lem  12518  dvds1lem  12519  dvds2lem  12520  odd2np1lem  12589  odd2np1  12590  opeo  12614  omeo  12615  divalglemex  12639  bezoutlemnewy  12723  bezoutlemaz  12730  bezoutlembz  12731  bezoutlemsup  12736  nnwodc  12763  uzwodc  12764  ncoprmgcdne1b  12817  exprmfct  12866  reumodprminv  12982  modprm0  12983  nnnn0modprm0  12984  pythagtriplem19  13011  pcprmpw2  13062  pockthi  13087  infpnlem2  13089  ballotfilem4  13191  ballotfilemic  13200  ennnfonelemex  13255  ennnfonelemhom  13256  ennnfonelemrn  13260  ennnfonelemnn0  13263  ennnfonelemim  13265  exmidunben  13267  ctinfomlemom  13268  ctinfom  13269  ctinf  13271  ctiunctlemf  13279  ismgmid2  13649  mgmidsssn0  13653  ismndd  13704  isgrpd2  13782  isgrpd  13784  imasgrp2  13869  mhmmnd  13875  ghmgrp  13877  dvdsrmuld  14347  dvdsr01  14355  rhmdvdsr  14426  lspf  14669  lspval  14670  lssats2  14694  fiinbas  15046  topbas  15064  clsval  15108  neiint  15142  neipsm  15151  opnneissb  15152  opnssneib  15153  innei  15160  restbasg  15165  lmconst  15213  iscnp4  15215  cncnpi  15225  cnconst2  15230  cnptoprest  15236  cnpdis  15239  neitx  15265  txcnp  15268  blssps  15424  blss  15425  blssexps  15426  blssex  15427  ssblex  15428  blin2  15429  neibl  15488  metss2  15495  bdmopn  15501  metrest  15503  metcnp3  15508  tgioo  15551  tgqioo  15552  addcncntoplem  15558  cnopnap  15608  dedekindeulemuub  15614  suplociccreex  15621  dedekindicclemuub  15623  ivthinclemlm  15631  ivthinclemum  15632  ivthinclemlopn  15633  ivthinclemuopn  15635  ivthreinc  15642  elply2  15732  reeff1oleme  15769  sin0pilem2  15779  sgmnncl  15988  dvdsppwf1o  15989  perfect  16001  bj-nn0suc0  16862  bj-inf2vnlem1  16882  3dom  16904  nninfsellemeq  16934  nninfomnilem  16938  qdencn  16949  trirec0  16970  qdiff  16975