Theorem rspcev 2701

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

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   = wceq 1284   ∈ wcel 1433  ∃wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603

This theorem is referenced by:  rspc2ev  2715  rspc3ev  2717  reu6i  2783  rspesbca  2898  nn0suc  4345  elrnmpt1s  4602  elrnrexdm  5327  eldmrexrn  5329  foco2  5339  elabrex  5418  f1elima  5433  fcofo  5444  fliftfun  5456  fliftval  5460  f1oiso2  5486  fo1st  5804  fo2nd  5805  tfr0  5960  tfrlemisucaccv  5962  tfrlemi14d  5970  tfrexlem  5971  rdgss  5993  nnaordex  6123  nnawordex  6124  ecelqsg  6182  snfig  6314  nnfi  6357  findcard  6372  unsnfi  6384  eqsupti  6409  supmaxti  6417  supisoex  6422  infminti  6440  isnumi  6451  oncardval  6455  archnqq  6607  prarloclemarch2  6609  prcdnql  6674  prcunqu  6675  prarloclemlo  6684  prarloclem5  6690  nqprm  6732  1idprl  6780  1idpru  6781  ltexpri  6803  prplnqu  6810  recexprlemm  6814  recexprlem1ssl  6823  recexprlem1ssu  6824  recexpr  6828  aptiprleml  6829  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemloc  6842  cauappcvgprlem1  6849  cauappcvgprlem2  6850  cauappcvgpr  6852  caucvgprlemm  6858  caucvgprlemloc  6865  caucvgprlem1  6869  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgprpr  6902  negexsr  6949  recexgt0sr  6950  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  axrnegex  7045  axprecex  7046  nntopi  7060  axcaucvglemres  7065  cnegex  7286  recexre  7678  recexap  7743  receuap  7759  cju  8038  nn2ge  8071  nominpos  8268  zdiv  8435  btwnz  8466  supinfneg  8683  infsupneg  8684  ublbneg  8698  lbzbi  8701  zq  8711  z2ge  8893  iccsupr  8989  qbtwnzlemstep  9257  qbtwnzlemex  9259  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnre  9265  qbtwnxr  9266  expnbnd  9596  shftlem  9704  shftfvalg  9706  shftfval  9709  caucvgre  9867  cvg1nlemres  9871  rexanuz  9874  rexuz3  9876  resqrexlemex  9911  caubnd2  10003  maxabslemval  10094  maxleast  10099  rexanre  10106  rexico  10107  fimaxre2  10109  minmax  10112  climconst  10129  climshftlemg  10141  cn1lem  10152  serif0  10189  dvdsval2  10198  dvds0lem  10205  dvds1lem  10206  dvds2lem  10207  odd2np1lem  10271  odd2np1  10272  opeo  10297  omeo  10298  divalglemex  10322  zsupcllemstep  10341  infssuzex  10345  bezoutlemnewy  10385  bezoutlemaz  10392  bezoutlembz  10393  bezoutlemsup  10398  ncoprmgcdne1b  10471  exprmfct  10519  bj-nn0suc0  10745  bj-inf2vnlem1  10765  qdencn  10785