Theorem rspcev 2881

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2177  ∃wrex 2486

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775

This theorem is referenced by:  rspceaimv  2889  rspc2ev  2896  rspc3ev  2898  rspceeqv  2899  reu6i  2968  rspesbca  3087  brralrspcev  4110  nn0suc  4660  elrnmpt1s  4937  elrnrexdm  5732  eldmrexrn  5734  foco2  5835  elabrex  5839  elabrexg  5840  f1elima  5855  fcofo  5866  fliftfun  5878  fliftval  5882  f1oiso2  5909  fo1st  6256  fo2nd  6257  tfr0dm  6421  tfrlemisucaccv  6424  tfrlemi14d  6432  tfrexlem  6433  tfr1onlemsucaccv  6440  tfr1onlemres  6448  tfrcllemsucaccv  6453  tfrcllemres  6461  rdgss  6482  frecabcl  6498  nnaordex  6627  nnawordex  6628  ecelqsg  6688  snfig  6920  nnfi  6984  findcard  7000  fimax2gtrilemstep  7012  unsnfi  7031  eqsupti  7113  supmaxti  7121  supisoex  7126  infminti  7144  finomni  7257  nninfwlpoimlemginf  7293  isnumi  7304  oncardval  7308  archnqq  7550  prarloclemarch2  7552  prcdnql  7617  prcunqu  7618  prarloclemlo  7627  prarloclem5  7633  nqprm  7675  1idprl  7723  1idpru  7724  ltexpri  7746  prplnqu  7753  recexprlemm  7757  recexprlem1ssl  7766  recexprlem1ssu  7767  recexpr  7771  aptiprleml  7772  archpr  7776  cauappcvgprlemm  7778  cauappcvgprlemloc  7785  cauappcvgprlem1  7792  cauappcvgprlem2  7793  cauappcvgpr  7795  caucvgprlemm  7801  caucvgprlemloc  7808  caucvgprlem1  7812  caucvgprlem2  7813  caucvgpr  7815  caucvgprprlemmu  7828  caucvgprprlemopl  7830  caucvgprprlemopu  7832  caucvgprprlemloc  7836  caucvgprprlem1  7842  caucvgprprlem2  7843  caucvgprpr  7845  suplocexprlemmu  7851  suplocexprlemloc  7854  suplocexpr  7858  negexsr  7905  recexgt0sr  7906  caucvgsrlemgt1  7928  caucvgsrlemoffres  7933  suplocsrlem  7941  axrnegex  8012  axprecex  8013  nntopi  8027  axcaucvglemres  8032  axpre-suploclemres  8034  cnegex  8270  recexre  8671  recexap  8746  receuap  8762  rerecapb  8936  sup3exmid  9050  cju  9054  nn2ge  9089  nominpos  9295  zdiv  9481  btwnz  9512  supinfneg  9736  infsupneg  9737  ublbneg  9754  lbzbi  9757  zq  9767  z2ge  9968  iccsupr  10108  zsupcllemstep  10394  infssuzex  10398  suprzubdc  10401  zsupssdc  10403  exbtwnzlemstep  10412  exbtwnzlemex  10414  rebtwn2zlemstep  10417  rebtwn2z  10419  qbtwnre  10421  qbtwnxr  10422  expnbnd  10830  hashunlem  10971  iswrdinn0  11021  shftlem  11202  shftfvalg  11204  shftfval  11207  caucvgre  11367  cvg1nlemres  11371  rexanuz  11374  rexuz3  11376  resqrexlemex  11411  caubnd2  11503  maxabslemval  11594  maxleast  11599  rexanre  11606  rexico  11607  fimaxre2  11613  minmax  11616  xrmaxiflemval  11636  xrmaxaddlem  11646  xrminmax  11651  climconst  11676  climshftlemg  11688  cn1lem  11700  serf0  11738  zsumdc  11770  fsum3  11773  fsum3cvg3  11782  mertenslemi1  11921  ntrivcvgap0  11935  zproddc  11965  fprodseq  11969  fprodntrivap  11970  dvdsval2  12176  dvds0lem  12187  dvds1lem  12188  dvds2lem  12189  odd2np1lem  12258  odd2np1  12259  opeo  12283  omeo  12284  divalglemex  12308  bezoutlemnewy  12392  bezoutlemaz  12399  bezoutlembz  12400  bezoutlemsup  12405  nnwodc  12432  uzwodc  12433  ncoprmgcdne1b  12486  exprmfct  12535  reumodprminv  12651  modprm0  12652  nnnn0modprm0  12653  pythagtriplem19  12680  pcprmpw2  12731  pockthi  12756  infpnlem2  12758  ennnfonelemex  12860  ennnfonelemhom  12861  ennnfonelemrn  12865  ennnfonelemnn0  12868  ennnfonelemim  12870  exmidunben  12872  ctinfomlemom  12873  ctinfom  12874  ctinf  12876  ctiunctlemf  12884  ismgmid2  13287  mgmidsssn0  13291  ismndd  13344  isgrpd2  13428  isgrpd  13430  imasgrp2  13521  mhmmnd  13527  ghmgrp  13529  dvdsrmuld  13933  dvdsr01  13941  rhmdvdsr  14012  lspf  14226  lspval  14227  lssats2  14251  fiinbas  14596  topbas  14614  clsval  14658  neiint  14692  neipsm  14701  opnneissb  14702  opnssneib  14703  innei  14710  restbasg  14715  lmconst  14763  iscnp4  14765  cncnpi  14775  cnconst2  14780  cnptoprest  14786  cnpdis  14789  neitx  14815  txcnp  14818  blssps  14974  blss  14975  blssexps  14976  blssex  14977  ssblex  14978  blin2  14979  neibl  15038  metss2  15045  bdmopn  15051  metrest  15053  metcnp3  15058  tgioo  15101  tgqioo  15102  addcncntoplem  15108  cnopnap  15158  dedekindeulemuub  15164  suplociccreex  15171  dedekindicclemuub  15173  ivthinclemlm  15181  ivthinclemum  15182  ivthinclemlopn  15183  ivthinclemuopn  15185  ivthreinc  15192  elply2  15282  reeff1oleme  15319  sin0pilem2  15329  sgmnncl  15535  dvdsppwf1o  15536  perfect  15548  bj-nn0suc0  16024  bj-inf2vnlem1  16044  nninfsellemeq  16092  nninfomnilem  16096  qdencn  16107  trirec0  16124