Theorem rspcev 2868

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765

This theorem is referenced by:  rspceaimv  2876  rspc2ev  2883  rspc3ev  2885  rspceeqv  2886  reu6i  2955  rspesbca  3074  brralrspcev  4092  nn0suc  4641  elrnmpt1s  4917  elrnrexdm  5704  eldmrexrn  5706  foco2  5803  elabrex  5807  elabrexg  5808  f1elima  5823  fcofo  5834  fliftfun  5846  fliftval  5850  f1oiso2  5877  fo1st  6224  fo2nd  6225  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemsucaccv  6408  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllemres  6429  rdgss  6450  frecabcl  6466  nnaordex  6595  nnawordex  6596  ecelqsg  6656  snfig  6882  nnfi  6942  findcard  6958  fimax2gtrilemstep  6970  unsnfi  6989  eqsupti  7071  supmaxti  7079  supisoex  7084  infminti  7102  finomni  7215  nninfwlpoimlemginf  7251  isnumi  7260  oncardval  7264  archnqq  7501  prarloclemarch2  7503  prcdnql  7568  prcunqu  7569  prarloclemlo  7578  prarloclem5  7584  nqprm  7626  1idprl  7674  1idpru  7675  ltexpri  7697  prplnqu  7704  recexprlemm  7708  recexprlem1ssl  7717  recexprlem1ssu  7718  recexpr  7722  aptiprleml  7723  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemloc  7736  cauappcvgprlem1  7743  cauappcvgprlem2  7744  cauappcvgpr  7746  caucvgprlemm  7752  caucvgprlemloc  7759  caucvgprlem1  7763  caucvgprlem2  7764  caucvgpr  7766  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgprpr  7796  suplocexprlemmu  7802  suplocexprlemloc  7805  suplocexpr  7809  negexsr  7856  recexgt0sr  7857  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  suplocsrlem  7892  axrnegex  7963  axprecex  7964  nntopi  7978  axcaucvglemres  7983  axpre-suploclemres  7985  cnegex  8221  recexre  8622  recexap  8697  receuap  8713  rerecapb  8887  sup3exmid  9001  cju  9005  nn2ge  9040  nominpos  9246  zdiv  9431  btwnz  9462  supinfneg  9686  infsupneg  9687  ublbneg  9704  lbzbi  9707  zq  9717  z2ge  9918  iccsupr  10058  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  zsupssdc  10345  exbtwnzlemstep  10354  exbtwnzlemex  10356  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnre  10363  qbtwnxr  10364  expnbnd  10772  hashunlem  10913  iswrdinn0  10957  shftlem  10998  shftfvalg  11000  shftfval  11003  caucvgre  11163  cvg1nlemres  11167  rexanuz  11170  rexuz3  11172  resqrexlemex  11207  caubnd2  11299  maxabslemval  11390  maxleast  11395  rexanre  11402  rexico  11403  fimaxre2  11409  minmax  11412  xrmaxiflemval  11432  xrmaxaddlem  11442  xrminmax  11447  climconst  11472  climshftlemg  11484  cn1lem  11496  serf0  11534  zsumdc  11566  fsum3  11569  fsum3cvg3  11578  mertenslemi1  11717  ntrivcvgap0  11731  zproddc  11761  fprodseq  11765  fprodntrivap  11766  dvdsval2  11972  dvds0lem  11983  dvds1lem  11984  dvds2lem  11985  odd2np1lem  12054  odd2np1  12055  opeo  12079  omeo  12080  divalglemex  12104  bezoutlemnewy  12188  bezoutlemaz  12195  bezoutlembz  12196  bezoutlemsup  12201  nnwodc  12228  uzwodc  12229  ncoprmgcdne1b  12282  exprmfct  12331  reumodprminv  12447  modprm0  12448  nnnn0modprm0  12449  pythagtriplem19  12476  pcprmpw2  12527  pockthi  12552  infpnlem2  12554  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemrn  12661  ennnfonelemnn0  12664  ennnfonelemim  12666  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  ctinf  12672  ctiunctlemf  12680  ismgmid2  13082  mgmidsssn0  13086  ismndd  13139  isgrpd2  13223  isgrpd  13225  imasgrp2  13316  mhmmnd  13322  ghmgrp  13324  dvdsrmuld  13728  dvdsr01  13736  rhmdvdsr  13807  lspf  14021  lspval  14022  lssats2  14046  fiinbas  14369  topbas  14387  clsval  14431  neiint  14465  neipsm  14474  opnneissb  14475  opnssneib  14476  innei  14483  restbasg  14488  lmconst  14536  iscnp4  14538  cncnpi  14548  cnconst2  14553  cnptoprest  14559  cnpdis  14562  neitx  14588  txcnp  14591  blssps  14747  blss  14748  blssexps  14749  blssex  14750  ssblex  14751  blin2  14752  neibl  14811  metss2  14818  bdmopn  14824  metrest  14826  metcnp3  14831  tgioo  14874  tgqioo  14875  addcncntoplem  14881  cnopnap  14931  dedekindeulemuub  14937  suplociccreex  14944  dedekindicclemuub  14946  ivthinclemlm  14954  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthreinc  14965  elply2  15055  reeff1oleme  15092  sin0pilem2  15102  sgmnncl  15308  dvdsppwf1o  15309  perfect  15321  bj-nn0suc0  15680  bj-inf2vnlem1  15700  nninfsellemeq  15745  nninfomnilem  15749  qdencn  15758  trirec0  15775