Theorem rspcev 2758

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1312   ∈ wcel 1461  ∃wrex 2389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-v 2657

This theorem is referenced by:  rspceaimv  2765  rspc2ev  2772  rspc3ev  2774  rspceeqv  2775  reu6i  2842  rspesbca  2959  nn0suc  4476  elrnmpt1s  4747  elrnrexdm  5511  eldmrexrn  5513  foco2  5607  elabrex  5611  f1elima  5626  fcofo  5637  fliftfun  5649  fliftval  5653  f1oiso2  5680  fo1st  6006  fo2nd  6007  tfr0dm  6170  tfrlemisucaccv  6173  tfrlemi14d  6181  tfrexlem  6182  tfr1onlemsucaccv  6189  tfr1onlemres  6197  tfrcllemsucaccv  6202  tfrcllemres  6210  rdgss  6231  frecabcl  6247  nnaordex  6374  nnawordex  6375  ecelqsg  6433  snfig  6659  nnfi  6716  findcard  6732  fimax2gtrilemstep  6744  unsnfi  6757  eqsupti  6832  supmaxti  6840  supisoex  6845  infminti  6863  finomni  6959  isnumi  6984  oncardval  6988  archnqq  7166  prarloclemarch2  7168  prcdnql  7233  prcunqu  7234  prarloclemlo  7243  prarloclem5  7249  nqprm  7291  1idprl  7339  1idpru  7340  ltexpri  7362  prplnqu  7369  recexprlemm  7373  recexprlem1ssl  7382  recexprlem1ssu  7383  recexpr  7387  aptiprleml  7388  archpr  7392  cauappcvgprlemm  7394  cauappcvgprlemloc  7401  cauappcvgprlem1  7408  cauappcvgprlem2  7409  cauappcvgpr  7411  caucvgprlemm  7417  caucvgprlemloc  7424  caucvgprlem1  7428  caucvgprlem2  7429  caucvgpr  7431  caucvgprprlemmu  7444  caucvgprprlemopl  7446  caucvgprprlemopu  7448  caucvgprprlemloc  7452  caucvgprprlem1  7458  caucvgprprlem2  7459  caucvgprpr  7461  negexsr  7508  recexgt0sr  7509  caucvgsrlemgt1  7530  caucvgsrlemoffres  7535  axrnegex  7607  axprecex  7608  nntopi  7622  axcaucvglemres  7627  cnegex  7856  recexre  8251  recexap  8320  receuap  8336  sup3exmid  8618  cju  8622  nn2ge  8656  nominpos  8854  zdiv  9036  btwnz  9067  supinfneg  9285  infsupneg  9286  ublbneg  9300  lbzbi  9303  zq  9313  z2ge  9495  iccsupr  9635  exbtwnzlemstep  9911  exbtwnzlemex  9913  rebtwn2zlemstep  9916  rebtwn2z  9918  qbtwnre  9920  qbtwnxr  9921  expnbnd  10301  hashunlem  10436  shftlem  10474  shftfvalg  10476  shftfval  10479  caucvgre  10638  cvg1nlemres  10642  rexanuz  10645  rexuz3  10647  resqrexlemex  10682  caubnd2  10774  maxabslemval  10865  maxleast  10870  rexanre  10877  rexico  10878  fimaxre2  10883  minmax  10886  xrmaxiflemval  10904  xrmaxaddlem  10914  xrminmax  10919  climconst  10944  climshftlemg  10956  cn1lem  10968  serf0  11006  zsumdc  11038  fsum3  11041  fsum3cvg3  11050  mertenslemi1  11189  dvdsval2  11337  dvds0lem  11344  dvds1lem  11345  dvds2lem  11346  odd2np1lem  11410  odd2np1  11411  opeo  11435  omeo  11436  divalglemex  11460  zsupcllemstep  11479  infssuzex  11483  bezoutlemnewy  11523  bezoutlemaz  11530  bezoutlembz  11531  bezoutlemsup  11536  ncoprmgcdne1b  11609  exprmfct  11657  ennnfonelemex  11765  ennnfonelemhom  11766  ennnfonelemrn  11770  ennnfonelemnn0  11773  ennnfonelemim  11775  exmidunben  11777  ctinfomlemom  11778  ctinfom  11779  ctinf  11781  ctiunctlemf  11787  fiinbas  12052  topbas  12072  clsval  12116  neiint  12150  neipsm  12159  opnneissb  12160  opnssneib  12161  innei  12168  restbasg  12173  lmconst  12220  iscnp4  12222  cncnpi  12232  cnconst2  12237  cnptoprest  12243  cnpdis  12246  neitx  12272  txcnp  12275  blssps  12409  blss  12410  blssexps  12411  blssex  12412  ssblex  12413  blin2  12414  neibl  12473  metss2  12480  bdmopn  12486  metrest  12488  metcnp3  12493  tgioo  12525  tgqioo  12526  addcncntoplem  12530  bj-nn0suc0  12827  bj-inf2vnlem1  12847  nninfsellemeq  12887  nninfomnilem  12891  qdencn  12899